equal
deleted
inserted
replaced
74 Facts that are introduced by invoking the case context are uniformly |
74 Facts that are introduced by invoking the case context are uniformly |
75 qualified by "a"; the same name is used for the cumulative fact. The old |
75 qualified by "a"; the same name is used for the cumulative fact. The old |
76 form "case (c xs) [attributes]" is no longer supported. Rare |
76 form "case (c xs) [attributes]" is no longer supported. Rare |
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 |
|
80 * Proof method "goals" turns the current subgoals into cases within the |
|
81 context; the conclusion is bound to variable ?case in each case. |
79 |
82 |
80 * Nesting of Isar goal structure has been clarified: the context after |
83 * Nesting of Isar goal structure has been clarified: the context after |
81 the initial backwards refinement is retained for the whole proof, within |
84 the initial backwards refinement is retained for the whole proof, within |
82 all its context sections (as indicated via 'next'). This is e.g. |
85 all its context sections (as indicated via 'next'). This is e.g. |
83 relevant for 'using', 'including', 'supply': |
86 relevant for 'using', 'including', 'supply': |