# HG changeset patch
# User wenzelm
# Date 1307799406 -7200
# Node ID 9cbcab5c780a02760228e0267a9b55cf01fc076c
# Parent  f8944cb2468f416be1ea5ca1a41165fbc25cede8
moved/updated single-step tactics;

diff -r f8944cb2468f -r 9cbcab5c780a doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:03:31 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:36:46 2011 +0200
@@ -1068,13 +1068,8 @@
   \item @{method safe} repeatedly performs safe steps on all subgoals.
   It is deterministic, with at most one outcome.
 
-  \item @{method clarify} performs a series of safe steps as follows.
-
-  No splitting step is applied; for example, the subgoal @{text "A \<and>
-  B"} is left as a conjunction.  Proof by assumption, Modus Ponens,
-  etc., may be performed provided they do not instantiate unknowns.
-  Assumptions of the form @{text "x = t"} may be eliminated.  The safe
-  wrapper tactical is applied.
+  \item @{method clarify} performs a series of safe steps without
+  splitting subgoals; see also @{ML clarify_step_tac}.
 
   \item @{method clarsimp} acts like @{method clarify}, but also does
   simplification.  Note that if the Simplifier context includes a
@@ -1084,6 +1079,52 @@
 *}
 
 
+subsection {* Single-step tactics *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
+    @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
+    @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
+    @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
+    @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
+  \end{matharray}
+
+  These are the primitive tactics behind the (semi)automated proof
+  methods of the Classical Reasoner.  By calling them yourself, you
+  can execute these procedures one step at a time.
+
+  \begin{description}
+
+  \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
+  subgoal @{text i}.  The safe wrapper tacticals are applied to a
+  tactic that may include proof by assumption or Modus Ponens (taking
+  care not to instantiate unknowns), or substitution.
+
+  \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
+  unknowns to be instantiated.
+
+  \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
+  procedure.  The unsafe wrapper tacticals are applied to a tactic
+  that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
+  rule from the context.
+
+  \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
+  backtracking between using safe rules with instantiation (@{ML
+  inst_step_tac}) and using unsafe rules.  The resulting search space
+  is larger.
+
+  \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
+  on subgoal @{text i}.  No splitting step is applied; for example,
+  the subgoal @{text "A \<and> B"} is left as a conjunction.  Proof by
+  assumption, Modus Ponens, etc., may be performed provided they do
+  not instantiate unknowns.  Assumptions of the form @{text "x = t"}
+  may be eliminated.  The safe wrapper tactical is applied.
+
+  \end{description}
+*}
+
+
 section {* Object-logic setup \label{sec:object-logic} *}
 
 text {*
diff -r f8944cb2468f -r 9cbcab5c780a doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:03:31 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:36:46 2011 +0200
@@ -1656,12 +1656,8 @@
   \item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
   It is deterministic, with at most one outcome.
 
-  \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps as follows.
-
-  No splitting step is applied; for example, the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction.  Proof by assumption, Modus Ponens,
-  etc., may be performed provided they do not instantiate unknowns.
-  Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} may be eliminated.  The safe
-  wrapper tactical is applied.
+  \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps without
+  splitting subgoals; see also \verb|clarify_step_tac|.
 
   \item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
   simplification.  Note that if the Simplifier context includes a
@@ -1671,6 +1667,53 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Single-step tactics%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{ML}{safe\_step\_tac}\verb|safe_step_tac: Proof.context -> int -> tactic| \\
+    \indexdef{}{ML}{inst\_step\_tac}\verb|inst_step_tac: Proof.context -> int -> tactic| \\
+    \indexdef{}{ML}{step\_tac}\verb|step_tac: Proof.context -> int -> tactic| \\
+    \indexdef{}{ML}{slow\_step\_tac}\verb|slow_step_tac: Proof.context -> int -> tactic| \\
+    \indexdef{}{ML}{clarify\_step\_tac}\verb|clarify_step_tac: Proof.context -> int -> tactic| \\
+  \end{matharray}
+
+  These are the primitive tactics behind the (semi)automated proof
+  methods of the Classical Reasoner.  By calling them yourself, you
+  can execute these procedures one step at a time.
+
+  \begin{description}
+
+  \item \verb|safe_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step on
+  subgoal \isa{i}.  The safe wrapper tacticals are applied to a
+  tactic that may include proof by assumption or Modus Ponens (taking
+  care not to instantiate unknowns), or substitution.
+
+  \item \verb|inst_step_tac| is like \verb|safe_step_tac|, but allows
+  unknowns to be instantiated.
+
+  \item \verb|step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} is the basic step of the proof
+  procedure.  The unsafe wrapper tacticals are applied to a tactic
+  that tries \verb|safe_tac|, \verb|inst_step_tac|, or applies an unsafe
+  rule from the context.
+
+  \item \verb|slow_step_tac| resembles \verb|step_tac|, but allows
+  backtracking between using safe rules with instantiation (\verb|inst_step_tac|) and using unsafe rules.  The resulting search space
+  is larger.
+
+  \item \verb|clarify_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step
+  on subgoal \isa{i}.  No splitting step is applied; for example,
+  the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction.  Proof by
+  assumption, Modus Ponens, etc., may be performed provided they do
+  not instantiate unknowns.  Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}}
+  may be eliminated.  The safe wrapper tactical is applied.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Object-logic setup \label{sec:object-logic}%
 }
 \isamarkuptrue%
diff -r f8944cb2468f -r 9cbcab5c780a doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Sat Jun 11 15:03:31 2011 +0200
+++ b/doc-src/Ref/classical.tex	Sat Jun 11 15:36:46 2011 +0200
@@ -125,21 +125,6 @@
 
 \section{The classical tactics}
 
-\subsection{Semi-automatic tactics}
-\begin{ttbox} 
-clarify_step_tac : claset -> int -> tactic
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
-  subgoal~$i$.  No splitting step is applied; for example, the subgoal $A\conj
-  B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be
-  performed provided they do not instantiate unknowns.  Assumptions of the
-  form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
-  applied.
-\end{ttdescription}
-
-
 \subsection{Other classical tactics}
 \begin{ttbox} 
 slow_best_tac : claset -> int -> tactic
@@ -173,36 +158,6 @@
 \end{ttdescription}
 
 
-\subsection{Single-step tactics}
-\begin{ttbox} 
-safe_step_tac : claset -> int -> tactic
-inst_step_tac : claset -> int -> tactic
-step_tac      : claset -> int -> tactic
-slow_step_tac : claset -> int -> tactic
-\end{ttbox}
-The automatic proof procedures call these tactics.  By calling them
-yourself, you can execute these procedures one step at a time.
-\begin{ttdescription}
-\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
-  subgoal~$i$.  The safe wrapper tacticals are applied to a tactic that may
-  include proof by assumption or Modus Ponens (taking care not to instantiate
-  unknowns), or substitution.
-
-\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
-but allows unknowns to be instantiated.
-
-\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
-  procedure.  The unsafe wrapper tacticals are applied to a tactic that tries
-  \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
-  from~$cs$.
-
-\item[\ttindexbold{slow_step_tac}] 
-  resembles \texttt{step_tac}, but allows backtracking between using safe
-  rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
-  The resulting search space is larger.
-\end{ttdescription}
-
-
 \subsection{Other useful tactics}
 \index{tactics!for contradiction}
 \index{tactics!for Modus Ponens}