-
Robbert Krebbers authored
- Support for a `//` modifier to close the goal using `done`. - Support for framing in the `[#]` specialization pattern for persistent premises, i.e. `[# $H1 $H2]` - Add new "auto framing patterns" `[$]`, `[# $]` and `>[$]` that will try to solve the premise by framing. Hypothesis that are not framed are carried over to the next goal.
87a8a19c