summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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