NEWS
changeset 60617 0eb41780449b
parent 60610 f52b4b0c10c4
child 60618 4c79543cc376
     1.1 --- a/NEWS	Mon Jun 29 23:44:53 2015 +0200
     1.2 +++ b/NEWS	Tue Jun 30 10:40:42 2015 +0200
     1.3 @@ -99,10 +99,22 @@
     1.4  
     1.5  * Proof method "goals" turns the current subgoals into cases within the
     1.6  context; the conclusion is bound to variable ?case in each case.
     1.7 +For example:
     1.8 +
     1.9 +lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
    1.10 +  and "\<And>y z. U y \<Longrightarrow> V u \<Longrightarrow> W y z"
    1.11 +proof goals
    1.12 +  case prems: 1
    1.13 +  then show ?case using prems sorry
    1.14 +next
    1.15 +  case prems: 2
    1.16 +  then show ?case using prems sorry
    1.17 +qed
    1.18  
    1.19  * The undocumented feature of implicit cases goal1, goal2, goal3, etc.
    1.20 -is marked as legacy, and will be removed eventually. Note that proof
    1.21 -method "goals" achieves a similar effect within regular Isar.
    1.22 +is marked as legacy, and will be removed eventually. The proof method
    1.23 +"goals" achieves a similar effect within regular Isar; often it can be
    1.24 +done more adequately by other means (e.g. 'consider').
    1.25  
    1.26  * Nesting of Isar goal structure has been clarified: the context after
    1.27  the initial backwards refinement is retained for the whole proof, within