
diff -r 7f9d7b55ea90 -r 41394a61cca9 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Sun Jun 05 20:23:05 2011 +0200
+++ b/doc-src/Ref/classical.tex	Sun Jun 05 22:02:54 2011 +0200
@@ -124,129 +124,28 @@
 
 
 \section{The classical tactics}
-\index{classical reasoner!tactics} If installed, the classical module provides
-powerful theorem-proving tactics.
-
-
-\subsection{The tableau prover}
-The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
-coded directly in \ML.  It then reconstructs the proof using Isabelle
-tactics.  It is faster and more powerful than the other classical
-reasoning tactics, but has major limitations too.
-\begin{itemize}
-\item It does not use the wrapper tacticals described above, such as
-  \ttindex{addss}.
-\item It does not perform higher-order unification, as needed by the rule {\tt
-    rangeI} in HOL and \texttt{RepFunI} in ZF.  There are often alternatives
-  to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
-\item Function variables may only be applied to parameters of the subgoal.
-(This restriction arises because the prover does not use higher-order
-unification.)  If other function variables are present then the prover will
-fail with the message {\small\tt Function Var's argument not a bound variable}.
-\item Its proof strategy is more general than \texttt{fast_tac}'s but can be
-  slower.  If \texttt{blast_tac} fails or seems to be running forever, try {\tt
-  fast_tac} and the other tactics described below.
-\end{itemize}
-%
-\begin{ttbox} 
-blast_tac        : claset -> int -> tactic
-Blast.depth_tac  : claset -> int -> int -> tactic
-Blast.trace      : bool ref \hfill{\bf initially false}
-\end{ttbox}
-The two tactics differ on how they bound the number of unsafe steps used in a
-proof.  While \texttt{blast_tac} starts with a bound of zero and increases it
-successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
-\begin{ttdescription}
-\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
-  subgoal~$i$, increasing the search bound using iterative
-  deepening~\cite{korf85}. 
-  
-\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
-  to prove subgoal~$i$ using a search bound of $lim$.  Sometimes a slow
-  proof using \texttt{blast_tac} can be made much faster by supplying the
-  successful search bound to this tactic instead.
-  
-\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
-  causes the tableau prover to print a trace of its search.  At each step it
-  displays the formula currently being examined and reports whether the branch
-  has been closed, extended or split.
-\end{ttdescription}
-
-
-\subsection{Automatic tactics}\label{sec:automatic-tactics}
-\begin{ttbox} 
-type clasimpset = claset * simpset;
-auto_tac        : clasimpset ->        tactic
-force_tac       : clasimpset -> int -> tactic
-auto            : unit -> unit
-force           : int  -> unit
-\end{ttbox}
-The automatic tactics attempt to prove goals using a combination of
-simplification and classical reasoning. 
-\begin{ttdescription}
-\item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where 
-there are a lot of mostly trivial subgoals; it proves all the easy ones, 
-leaving the ones it cannot prove.
-(Unfortunately, attempting to prove the hard ones may take a long time.)  
-\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ 
-completely. It tries to apply all fancy tactics it knows about, 
-performing a rather exhaustive search.
-\end{ttdescription}
-
 
 \subsection{Semi-automatic tactics}
 \begin{ttbox} 
-clarify_tac      : claset -> int -> tactic
 clarify_step_tac : claset -> int -> tactic
-clarsimp_tac     : clasimpset -> int -> tactic
 \end{ttbox}
-Use these when the automatic tactics fail.  They perform all the obvious
-logical inferences that do not split the subgoal.  The result is a
-simpler subgoal that can be tackled by other means, such as by
-instantiating quantifiers yourself.
+
 \begin{ttdescription}
-\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
-subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
 \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.
-\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
-also does simplification with the given simpset. Note that if the simpset 
-includes a splitter for the premises, the subgoal may still be split.
 \end{ttdescription}
 
 
 \subsection{Other classical tactics}
 \begin{ttbox} 
-fast_tac      : claset -> int -> tactic
-best_tac      : claset -> int -> tactic
-slow_tac      : claset -> int -> tactic
 slow_best_tac : claset -> int -> tactic
 \end{ttbox}
-These tactics attempt to prove a subgoal using sequent-style reasoning.
-Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle.  Their
-effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
-this subgoal or fail.  The \texttt{slow_} versions conduct a broader
-search.%
-\footnote{They may, when backtracking from a failed proof attempt, undo even
-  the step of proving a subgoal by assumption.}
 
-The best-first tactics are guided by a heuristic function: typically, the
-total size of the proof state.  This function is supplied in the functor call
-that sets up the classical reasoner.
 \begin{ttdescription}
-\item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
-depth-first search to prove subgoal~$i$.
-
-\item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
-best-first search to prove subgoal~$i$.
-
-\item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
-depth-first search to prove subgoal~$i$.
-
 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
 best-first search to prove subgoal~$i$.
 \end{ttdescription}
@@ -277,7 +176,6 @@
 \subsection{Single-step tactics}
 \begin{ttbox} 
 safe_step_tac : claset -> int -> tactic
-safe_tac      : claset        -> tactic
 inst_step_tac : claset -> int -> tactic
 step_tac      : claset -> int -> tactic
 slow_step_tac : claset -> int -> tactic
@@ -290,9 +188,6 @@
   include proof by assumption or Modus Ponens (taking care not to instantiate
   unknowns), or substitution.
 
-\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all 
-subgoals.  It is deterministic, with at most one outcome.  
-
 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
 but allows unknowns to be instantiated.
 




