[isabelle-dev] NEWS: cases from goals

Makarius makarius at sketis.net
Sat Jun 27 00:46:26 CEST 2015

* Proof method "goals" turns the current subgoals into cases within the
context; the conclusion is bound to variable ?case in each case.

* The undocumented feature of implicit cases goal1, goal2, goal3, etc.
is marked as legacy, and will be removed eventually. Note that proof
method "goals" achieves a similar effect within regular Isar.

This refers to c708dafe2220 and d2fbc021a44d. Example updates of oldd 
proofs are can be seen in changeset 7e741e22d7fc.


More information about the isabelle-dev mailing list