76 analogous to the 'rule_format' attribute, but *not* that of the 
76 analogous to the 'rule_format' attribute, but *not* that of the 
77 Simplifier (which is usually more generous). 
77 Simplifier (which is usually more generous). 
78 
78 
79 * Isar: the goal restriction operator [N] (default N = 1) evaluates a 
79 * Isar: the goal restriction operator [N] (default N = 1) evaluates a 
80 method expression within a sandbox consisting of the first N 
80 method expression within a sandbox consisting of the first N 
81 subgoals, which need to exist. (Recall that proper Isar proof methods 
81 subgoals, which need to exist. For example, ``simp_all [3]'' 
82 do not admit arbitrary goal addressing, unlike certain tactic 
82 simplifies the first three subgoals, while (rule foo, simp_all)[] 
83 emulations.) For example, ``simp_all [3]'' simplifies the first three 
83 simplifies all new goals that emerge from applying rule foo to the 
84 subgoals, while (rule foo, simp_all)[] simplifies all new goals that 
84 originally first one. 
85 emerge from applying rule foo to the originally first one. 

86 
85 
87 * Isar: the conclusion of a long theorem statement is now either 
86 * Isar: the conclusion of a long theorem statement is now either 
88 'shows' (a simultaneous conjunction, as before), or 'obtains' 
87 'shows' (a simultaneous conjunction, as before), or 'obtains' 
89 (essentially a disjunction of cases with local parameters and 
88 (essentially a disjunction of cases with local parameters and 
90 assumptions). The latter allows to express general elimination rules 
89 assumptions). The latter allows to express general elimination rules 