From 83256c1d0a15b2ce1506dccbb79a969452feeb22 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 1 May 2022 17:21:46 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ac6566191..10fbc83ae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,7 +21,8 @@ lemma.
    the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
 * `iInduction` now supports induction schemes that involve `Forall` and
   `Forall2` (for example, for trees with finite branching).
-* `iRevert` of a pure hypothesis generates a wand instead of an implication.
+* Change `iRevert` of a pure hypothesis to generate a magic wand instead of an
+  implication.
 
 **Changes in `base_logic`:**
 
-- 
GitLab