NEWS
changeset 19240 3a73cb17a707
parent 19233 77ca20b0ed77
child 19252 1f7c69a5faac
equal deleted inserted replaced
19239:31c114337224 19240:3a73cb17a707
    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 sub-goals, which need to exist. (Recall that proper Isar proof methods
    81 sub-goals, which need to exist.  For example, ``simp_all [3]''
    82 do not admit arbitrary goal addressing, unlike certain tactic
    82 simplifies the first three sub-goals, 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 sub-goals, 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