diff --git a/CHANGELOG.md b/CHANGELOG.md index ac6566191319dfe3d556f19ae414a389527df9d3..10fbc83ae2255664ffb5986d96982df336e34622 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`:**