1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:03:31 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:36:46 2011 +0200
     1.3 @@ -1656,12 +1656,8 @@
     1.4    \item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
     1.5    It is deterministic, with at most one outcome.
     1.6  
     1.7 -  \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps as follows.
     1.8 -
     1.9 -  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,
    1.10 -  etc., may be performed provided they do not instantiate unknowns.
    1.11 -  Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} may be eliminated.  The safe
    1.12 -  wrapper tactical is applied.
    1.13 +  \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps without
    1.14 +  splitting subgoals; see also \verb|clarify_step_tac|.
    1.15  
    1.16    \item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
    1.17    simplification.  Note that if the Simplifier context includes a
    1.18 @@ -1671,6 +1667,53 @@
    1.19  \end{isamarkuptext}%
    1.20  \isamarkuptrue%
    1.21  %
    1.22 +\isamarkupsubsection{Single-step tactics%
    1.23 +}
    1.24 +\isamarkuptrue%
    1.25 +%
    1.26 +\begin{isamarkuptext}%
    1.27 +\begin{matharray}{rcl}
    1.28 +    \indexdef{}{ML}{safe\_step\_tac}\verb|safe_step_tac: Proof.context -> int -> tactic| \\
    1.29 +    \indexdef{}{ML}{inst\_step\_tac}\verb|inst_step_tac: Proof.context -> int -> tactic| \\
    1.30 +    \indexdef{}{ML}{step\_tac}\verb|step_tac: Proof.context -> int -> tactic| \\
    1.31 +    \indexdef{}{ML}{slow\_step\_tac}\verb|slow_step_tac: Proof.context -> int -> tactic| \\
    1.32 +    \indexdef{}{ML}{clarify\_step\_tac}\verb|clarify_step_tac: Proof.context -> int -> tactic| \\
    1.33 +  \end{matharray}
    1.34 +
    1.35 +  These are the primitive tactics behind the (semi)automated proof
    1.36 +  methods of the Classical Reasoner.  By calling them yourself, you
    1.37 +  can execute these procedures one step at a time.
    1.38 +
    1.39 +  \begin{description}
    1.40 +
    1.41 +  \item \verb|safe_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step on
    1.42 +  subgoal \isa{i}.  The safe wrapper tacticals are applied to a
    1.43 +  tactic that may include proof by assumption or Modus Ponens (taking
    1.44 +  care not to instantiate unknowns), or substitution.
    1.45 +
    1.46 +  \item \verb|inst_step_tac| is like \verb|safe_step_tac|, but allows
    1.47 +  unknowns to be instantiated.
    1.48 +
    1.49 +  \item \verb|step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} is the basic step of the proof
    1.50 +  procedure.  The unsafe wrapper tacticals are applied to a tactic
    1.51 +  that tries \verb|safe_tac|, \verb|inst_step_tac|, or applies an unsafe
    1.52 +  rule from the context.
    1.53 +
    1.54 +  \item \verb|slow_step_tac| resembles \verb|step_tac|, but allows
    1.55 +  backtracking between using safe rules with instantiation (\verb|inst_step_tac|) and using unsafe rules.  The resulting search space
    1.56 +  is larger.
    1.57 +
    1.58 +  \item \verb|clarify_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step
    1.59 +  on subgoal \isa{i}.  No splitting step is applied; for example,
    1.60 +  the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction.  Proof by
    1.61 +  assumption, Modus Ponens, etc., may be performed provided they do
    1.62 +  not instantiate unknowns.  Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}}
    1.63 +  may be eliminated.  The safe wrapper tactical is applied.
    1.64 +
    1.65 +  \end{description}%
    1.66 +\end{isamarkuptext}%
    1.67 +\isamarkuptrue%
    1.68 +%
    1.69  \isamarkupsection{Object-logic setup \label{sec:object-logic}%
    1.70  }
    1.71  \isamarkuptrue%