From b5e2eb4e822720fb03720868e2b7970d3dcb4130 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Jul 2019 14:14:36 +0200
Subject: [PATCH] erasure is in iris/examples

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1b6f567af..54b56c618 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,7 +48,10 @@ Changes in heap_lang:
 * For consistency, the restrictions CmpXchg imposes on comparison also apply to
   the `=` binary operator. This also fixes the long-standing problem that that
   operator allowed compared closures with each other.
-* Implement prophecy variables using the new support for "observations".
+* Implement prophecy variables using the new support for "observations". The
+  erasure theorem (showing that prophecy variables do not alter program
+  behavior) can be found in the iris/examples repository, in
+  `theories/logatom/proph_erasure.rs`.
 * heap_lang now uses right-to-left evaluation order. This makes it
   significantly easier to write specifications of curried functions.
 * heap_lang values are now injected in heap_lang expressions via a specific
-- 
GitLab