--- 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}