[isabelle-dev] NEWS: cases from goals
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