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}