Commit 83256c1d authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 5f73bf42
Pipeline #65346 passed with stage
in 10 minutes and 25 seconds
......@@ -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`:**
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment