1.1 --- a/doc-src/Ref/classical.tex	Sat Jun 11 15:03:31 2011 +0200
     1.2 +++ b/doc-src/Ref/classical.tex	Sat Jun 11 15:36:46 2011 +0200
     1.3 @@ -125,21 +125,6 @@
     1.4  
     1.5  \section{The classical tactics}
     1.6  
     1.7 -\subsection{Semi-automatic tactics}
     1.8 -\begin{ttbox} 
     1.9 -clarify_step_tac : claset -> int -> tactic
    1.10 -\end{ttbox}
    1.11 -
    1.12 -\begin{ttdescription}
    1.13 -\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
    1.14 -  subgoal~$i$.  No splitting step is applied; for example, the subgoal $A\conj
    1.15 -  B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be
    1.16 -  performed provided they do not instantiate unknowns.  Assumptions of the
    1.17 -  form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
    1.18 -  applied.
    1.19 -\end{ttdescription}
    1.20 -
    1.21 -
    1.22  \subsection{Other classical tactics}
    1.23  \begin{ttbox} 
    1.24  slow_best_tac : claset -> int -> tactic
    1.25 @@ -173,36 +158,6 @@
    1.26  \end{ttdescription}
    1.27  
    1.28  
    1.29 -\subsection{Single-step tactics}
    1.30 -\begin{ttbox} 
    1.31 -safe_step_tac : claset -> int -> tactic
    1.32 -inst_step_tac : claset -> int -> tactic
    1.33 -step_tac      : claset -> int -> tactic
    1.34 -slow_step_tac : claset -> int -> tactic
    1.35 -\end{ttbox}
    1.36 -The automatic proof procedures call these tactics.  By calling them
    1.37 -yourself, you can execute these procedures one step at a time.
    1.38 -\begin{ttdescription}
    1.39 -\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
    1.40 -  subgoal~$i$.  The safe wrapper tacticals are applied to a tactic that may
    1.41 -  include proof by assumption or Modus Ponens (taking care not to instantiate
    1.42 -  unknowns), or substitution.
    1.43 -
    1.44 -\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
    1.45 -but allows unknowns to be instantiated.
    1.46 -
    1.47 -\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
    1.48 -  procedure.  The unsafe wrapper tacticals are applied to a tactic that tries
    1.49 -  \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
    1.50 -  from~$cs$.
    1.51 -
    1.52 -\item[\ttindexbold{slow_step_tac}] 
    1.53 -  resembles \texttt{step_tac}, but allows backtracking between using safe
    1.54 -  rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
    1.55 -  The resulting search space is larger.
    1.56 -\end{ttdescription}
    1.57 -
    1.58 -
    1.59  \subsection{Other useful tactics}
    1.60  \index{tactics!for contradiction}
    1.61  \index{tactics!for Modus Ponens}