--- a/doc-src/IsarRef/pure.tex Thu Mar 07 22:52:07 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Thu Mar 07 23:21:19 2002 +0100
@@ -1194,6 +1194,7 @@
\end{rail}
\begin{descr}
+
\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
$\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method
applications may be given just as in tactic scripts.
@@ -1229,6 +1230,7 @@
$\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so
$\isarkeyword{declare}$ only has the effect of applying attributes as
included in the theorem specification.
+
\end{descr}
Any proper Isar proof method may be used with tactic script commands such as