equal
deleted
inserted
replaced
77 INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, |
77 INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, |
78 and always put attributes in front. |
78 and always put attributes in front. |
79 |
79 |
80 * Proof method "goals" turns the current subgoals into cases within the |
80 * Proof method "goals" turns the current subgoals into cases within the |
81 context; the conclusion is bound to variable ?case in each case. |
81 context; the conclusion is bound to variable ?case in each case. |
|
82 |
|
83 * The undocumented feature of implicit cases goal1, goal2, goal3, etc. |
|
84 is marked as legacy, and will be removed eventually. Note that proof |
|
85 method "goals" achieves a similar effect within regular Isar. |
82 |
86 |
83 * Nesting of Isar goal structure has been clarified: the context after |
87 * Nesting of Isar goal structure has been clarified: the context after |
84 the initial backwards refinement is retained for the whole proof, within |
88 the initial backwards refinement is retained for the whole proof, within |
85 all its context sections (as indicated via 'next'). This is e.g. |
89 all its context sections (as indicated via 'next'). This is e.g. |
86 relevant for 'using', 'including', 'supply': |
90 relevant for 'using', 'including', 'supply': |