80 method expression within a sandbox consisting of the first N |
80 method expression within a sandbox consisting of the first N |
81 sub-goals, which need to exist. (Recall that proper Isar proof methods |
81 sub-goals, which need to exist. (Recall that proper Isar proof methods |
82 do not admit arbitrary goal addressing, unlike certain tactic |
82 do not admit arbitrary goal addressing, unlike certain tactic |
83 emulations.) For example, ``simp_all [3]'' simplifies the first three |
83 emulations.) For example, ``simp_all [3]'' simplifies the first three |
84 sub-goals, while (rule foo, simp_all)[] simplifies all new goals that |
84 sub-goals, while (rule foo, simp_all)[] simplifies all new goals that |
85 emerge from applying rule foo$to the originally first one. |
85 emerge from applying rule foo to the originally first one. |
86 |
86 |
87 * Isar: the conclusion of a long theorem statement is now either |
87 * Isar: the conclusion of a long theorem statement is now either |
88 'shows' (a simultaneous conjunction, as before), or 'obtains' |
88 'shows' (a simultaneous conjunction, as before), or 'obtains' |
89 (essentially a disjunction of cases with local parameters and |
89 (essentially a disjunction of cases with local parameters and |
90 assumptions). The latter allows to express general elimination rules |
90 assumptions). The latter allows to express general elimination rules |