[isabelle-dev] NEWS: cases from goals

[Makarius]

* 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