Commit 5f73bf42 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent e440e51b
Pipeline #65161 passed with stage
in 8 minutes and 33 seconds
......@@ -21,6 +21,7 @@ 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.
**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