From 33df52c8cffbbf1560967eac9ffd07f03e217196 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Oct 2018 10:01:08 +0200
Subject: [PATCH] changelog

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d93f562fe..a1ba54063 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,11 @@ Changes in and extensions of the theory:
   experimental.
 * [#] The adequacy statement for weakest preconditions now also involves the
   final state.
+* [#] Add the notion of an "observation" to the language interface, so that
+  every reduction step can optionally be marked with an event, and an execution
+  trace has a matching list of events.  Change WP so that it is told the entire
+  future trace of observations from the beginning.  Use this in heap_lang to
+  implement prophecy variables.
 * [#] The Löb rule is now a derived rule; it follows from later-intro, later
   being contractive and the fact that we can take fixpoints of contractive
   functions.
-- 
GitLab