[isabelle-dev] NEWS: cases from goals

[Makarius]

Here is an updated NEWS entry from Isabelle/0eb41780449b -- no changes, 
just more explanations:


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

lemma "⋀x. A x ⟹ B x ⟹ C x"
   and "⋀y z. U y ⟹ V u ⟹ W y z"
proof goals
   case prems: 1
   then show ?case using prems sorry
next
   case prems: 2
   then show ?case using prems sorry
qed

* The undocumented feature of implicit cases goal1, goal2, goal3, etc.
is marked as legacy, and will be removed eventually. The proof method
"goals" achieves a similar effect within regular Isar; often it can be
done more adequately by other means (e.g. 'consider').


Above I am using a new idiom, to name "prems" uniformly in each case. 
This helps to avoid specific names like "1", "2" etc. intrude the proof 
body.  Thus cases may be re-arranged later, without changing all the proof 
cases.

Moreover note, that the above example provides a solution to the 
occasional problem of ?thesis1, ?thesis2, etc. -- which are not provided 
by the system.  It just becomes ?case in each case.


 	Makarius