1.1 --- a/NEWS	Fri Mar 10 17:57:09 2006 +0100
     1.2 +++ b/NEWS	Fri Mar 10 19:49:58 2006 +0100
     1.3 @@ -78,11 +78,10 @@
     1.4  
     1.5  * Isar: the goal restriction operator [N] (default N = 1) evaluates a
     1.6  method expression within a sandbox consisting of the first N
     1.7 -sub-goals, which need to exist. (Recall that proper Isar proof methods
     1.8 -do not admit arbitrary goal addressing, unlike certain tactic
     1.9 -emulations.)  For example, ``simp_all [3]'' simplifies the first three
    1.10 -sub-goals, while (rule foo, simp_all)[] simplifies all new goals that
    1.11 -emerge from applying rule foo to the originally first one.
    1.12 +sub-goals, which need to exist.  For example, ``simp_all [3]''
    1.13 +simplifies the first three sub-goals, while (rule foo, simp_all)[]
    1.14 +simplifies all new goals that emerge from applying rule foo to the
    1.15 +originally first one.
    1.16  
    1.17  * Isar: the conclusion of a long theorem statement is now either
    1.18  'shows' (a simultaneous conjunction, as before), or 'obtains'