--- 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