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