diff -r 54acec31dcac -r 46bb6a4b3ac9 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Mar 20 18:43:05 2000 +0100
+++ b/doc-src/IsarRef/syntax.tex	Mon Mar 20 18:43:20 2000 +0100
@@ -294,6 +294,18 @@
   ;
 \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$.  In particular, $[1-]$ corresponds to the ML tactical \texttt{ALLGOALS}
+\cite{isabelle-ref}.
+
+\indexouternonterm{goalspec}
+\begin{rail}
+  goalspec: '[' (nat '-' nat | nat '-' | nat) ']'
+  ;
+\end{rail}
+
 
 %%% Local Variables: 
 %%% mode: latex