doc-src/IsarRef/pure.tex

--- a/doc-src/IsarRef/pure.tex	Wed May 31 14:14:45 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed May 31 14:14:59 2000 +0200
@@ -959,10 +959,6 @@
 
 \indexisarcmd{apply}\indexisarcmd{done}\indexisarcmd{apply-end}
 \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back}
-\indexisarmeth{tactic}\indexisarmeth{insert}
-\indexisarmeth{res-inst-tac}\indexisarmeth{eres-inst-tac}
-\indexisarmeth{dres-inst-tac}\indexisarmeth{forw-inst-tac}
-\indexisarmeth{subgoal-tac}
 \begin{matharray}{rcl}
   \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
   \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\
@@ -970,33 +966,11 @@
   \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
-  tactic^* & : & \isarmeth \\
-  insert^* & : & \isarmeth \\
-  res_inst_tac^* & : & \isarmeth \\
-  eres_inst_tac^* & : & \isarmeth \\
-  dres_inst_tac^* & : & \isarmeth \\
-  forw_inst_tac^* & : & \isarmeth \\
-  subgoal_tac^* & : & \isarmeth \\
 \end{matharray}
 
 \railalias{applyend}{apply\_end}
 \railterm{applyend}
 
-\railalias{resinsttac}{res\_inst\_tac}
-\railterm{resinsttac}
-
-\railalias{eresinsttac}{eres\_inst\_tac}
-\railterm{eresinsttac}
-
-\railalias{dresinsttac}{dres\_inst\_tac}
-\railterm{dresinsttac}
-
-\railalias{forwinsttac}{forw\_inst\_tac}
-\railterm{forwinsttac}
-
-\railalias{subgoaltac}{subgoal\_tac}
-\railterm{subgoaltac}
-
 \begin{rail}
   'apply' method comment?
   ;
@@ -1008,14 +982,6 @@
   ;
   'prefer' nat comment?
   ;
-  'tactic' text
-  ;
-  'insert' thmrefs
-  ;
-  ( resinsttac | eresinsttac | dresinsttac | forwinsttac ) goalspec? ((name '=' term) + 'and')
-  ;
-  subgoaltac goalspec? prop
-  ;
 \end{rail}
 
 \begin{descr}
@@ -1046,10 +1012,60 @@
   the latest proof command.\footnote{Unlike the ML function \texttt{back}
     \cite{isabelle-ref}, the Isar command does not search upwards for further
     branch points.} Basically, any proof command may return multiple results.
+\end{descr}
+
+Any proper Isar proof method may be used with tactic script commands such as
+$\isarkeyword{apply}$.  A few additional emulations of actual tactics are
+provided as well; these would be never used in actual structured proofs, of
+course.
+
+\indexisarmeth{tactic}\indexisarmeth{insert}
+\indexisarmeth{res-inst-tac}\indexisarmeth{eres-inst-tac}
+\indexisarmeth{dres-inst-tac}\indexisarmeth{forw-inst-tac}
+\indexisarmeth{subgoal-tac}
+\begin{matharray}{rcl}
+  tactic^* & : & \isarmeth \\
+  insert^* & : & \isarmeth \\
+  res_inst_tac^* & : & \isarmeth \\
+  eres_inst_tac^* & : & \isarmeth \\
+  dres_inst_tac^* & : & \isarmeth \\
+  forw_inst_tac^* & : & \isarmeth \\
+  subgoal_tac^* & : & \isarmeth \\
+\end{matharray}
+
+\railalias{resinsttac}{res\_inst\_tac}
+\railterm{resinsttac}
+
+\railalias{eresinsttac}{eres\_inst\_tac}
+\railterm{eresinsttac}
+
+\railalias{dresinsttac}{dres\_inst\_tac}
+\railterm{dresinsttac}
+
+\railalias{forwinsttac}{forw\_inst\_tac}
+\railterm{forwinsttac}
+
+\railalias{subgoaltac}{subgoal\_tac}
+\railterm{subgoaltac}
+
+\begin{rail}
+  'tactic' text
+  ;
+  'insert' thmrefs
+  ;
+  ( resinsttac | eresinsttac | dresinsttac | forwinsttac ) goalspec? \\
+    ((name '=' term) + 'and') 'in' thmref
+  ;
+  subgoaltac goalspec? prop
+  ;
+\end{rail}
+
+\begin{descr}
 \item [$tactic~text$] produces a proof method from any ML text of type
   \texttt{tactic}.  Apart from the usual ML environment and the current
   implicit theory context, the ML code may refer to the following locally
   bound values:
+
 %%FIXME ttbox produces too much trailing space (why?)
 {\footnotesize\begin{verbatim}
 val ctxt  : Proof.context