Isar/method: goal restriction;

--- a/NEWS	Wed Mar 08 18:37:24 2006 +0100
+++ b/NEWS	Wed Mar 08 18:37:25 2006 +0100
@@ -76,6 +76,14 @@
 analogous to the 'rule_format' attribute, but *not* that of the
 Simplifier (which is usually more generous).
 
+* 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.
+
 * Isar: the conclusion of a long theorem statement is now either
 'shows' (a simultaneous conjunction, as before), or 'obtains'
 (essentially a disjunction of cases with local parameters and

--- a/doc-src/IsarRef/syntax.tex	Wed Mar 08 18:37:24 2006 +0100
+++ b/doc-src/IsarRef/syntax.tex	Wed Mar 08 18:37:25 2006 +0100
@@ -291,24 +291,34 @@
 Proof methods are either basic ones, or expressions composed of
 methods via ``\texttt{,}'' (sequential composition), ``\texttt{|}''
 (alternative choices), ``\texttt{?}'' (try), ``\texttt{+}'' (repeat at
-least once), ``\texttt{[$n$]}'' (restriction to first $n$ sub-goals).
-In practice, proof methods are usually just a comma separated list of
-\railqtok{nameref}~\railnonterm{args} specifications.  Note that
-parentheses may be dropped for single method specifications (with no
-arguments).
+least once), ``\texttt{[$n$]}'' (restriction to first $n$ sub-goals,
+default $n = 1$).  In practice, proof methods are usually just a comma
+separated list of \railqtok{nameref}~\railnonterm{args}
+specifications.  Note that parentheses may be dropped for single
+method specifications (with no arguments).
 
 \indexouternonterm{method}
 \begin{rail}
-  method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat ']')
+  method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
   ;
   methods: (nameref args | method) + (',' | '|')
   ;
 \end{rail}
 
-Proper use of Isar proof methods does \emph{not} involve goal addressing.
-Nevertheless, specifying goal ranges may occasionally come in handy in
-emulating tactic scripts.  Note that $[n-]$ refers to all goals, starting from
-$n$.  All goals may be specified by $[!]$, which is the same as $[1-]$.
+Proper Isar proof methods do \emph{not} admit arbitrary goal
+addressing, but refer either to the first sub-goal or all sub-goals
+uniformly.  The goal restriction operator ``\texttt{[$n$]}'' evaluates
+a method expression within a sandbox consisting of the first $n$
+sub-goals (which need to exist).  For example,
+$simp_all\mbox{\tt[}3\mbox{\tt]}$ simplifies the first three
+sub-goals, while $(rule~foo, simp_all)\mbox{\tt[]}$ simplifies all new
+goals that emerge from applying rule $foo$ to the originally first
+one.
+
+Improper methods, notably tactic emulations, offer a separate
+low-level goal addressing scheme as explicit argument to the
+individual tactic being involved.  Here $[!]$ refers to all goals, and
+$[n-]$ to all goals starting from $n$,
 
 \indexouternonterm{goalspec}
 \begin{rail}