# HG changeset patch
# User wenzelm
# Date 953574200 -3600
# Node ID 46bb6a4b3ac9f2aac2cced518c3fb11c3c4e3e41
# Parent  54acec31dcacd1fd399b8d39c46471010a2f031f
goalspec;

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