* 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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
