# HG changeset patch
# User lcp
# Date 790912999 -3600
# Node ID a0b71a4bbe5efbeef2f98180b62afde098dc4b24
# Parent  2432820efbfeaa9e200ba019718b6fd57c27a617
documented slow_tac, slow_best_tac, depth_tac, deepen_tac

diff -r 2432820efbfe -r a0b71a4bbe5e doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Tue Jan 24 03:02:01 1995 +0100
+++ b/doc-src/Ref/classical.tex	Tue Jan 24 03:03:19 1995 +0100
@@ -266,20 +266,53 @@
 
 \subsection{The automatic tactics}
 \begin{ttbox} 
-fast_tac : claset -> int -> tactic
-best_tac : claset -> int -> tactic
+fast_tac      : claset -> int -> tactic
+best_tac      : claset -> int -> tactic
+slow_tac      : claset -> int -> tactic
+slow_best_tac : claset -> int -> tactic
 \end{ttbox}
-Both of these tactics work by applying {\tt step_tac} repeatedly.  Their
-effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
-solve this subgoal or fail.
+These tactics work by applying {\tt step_tac} or {\tt slow_step_tac}
+repeatedly.  Their effect is restricted (by {\tt SELECT_GOAL}) to one subgoal;
+they either solve this subgoal or fail.  The {\tt slow_} versions are more
+powerful but can be much slower.  
+
+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 {\tt step_tac} using
 depth-first search, to solve subgoal~$i$.
 
 \item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
-best-first search, to solve subgoal~$i$.  A heuristic function ---
-typically, the total size of the proof state --- guides the search.  This
-function is supplied when the classical reasoner is set up.
+best-first search, to solve subgoal~$i$.
+
+\item[\ttindexbold{slow_tac} $cs$ $i$] applies {\tt slow_step_tac} using
+depth-first search, to solve subgoal~$i$.
+
+\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies {\tt slow_step_tac} using
+best-first search, to solve subgoal~$i$.
+\end{ttdescription}
+
+
+\subsection{Depth-limited tactics}
+\begin{ttbox} 
+depth_tac  : claset -> int -> int -> tactic
+deepen_tac : claset -> int -> int -> tactic
+\end{ttbox}
+These work by exhaustive search up to a specified depth.  Unsafe rules are
+modified to preserve the formula they act on, so that it be used repeatedly.
+They can prove more goals than {\tt fast_tac}, etc., can.  They are much
+slower, for example if the assumptions have many universal quantifiers.
+
+The depth limits the number of unsafe steps.  If you can estimate the minimum
+number of unsafe steps needed, supply this value as~$m$ to save time.
+\begin{ttdescription}
+\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
+tries to solve subgoal~$i$ by exhaustive search up to depth~$m$.
+
+\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
+tries to solve subgoal~$i$ by iterative deepening.  It calls {\tt depth_tac}
+repeatedly with increasing depths, starting with~$m$.
 \end{ttdescription}
 
 
@@ -313,9 +346,7 @@
 \item[\ttindexbold{slow_step_tac}] 
   resembles {\tt step_tac}, but allows backtracking between using safe
   rules with instantiation ({\tt inst_step_tac}) and using unsafe rules.
-  The resulting search space is too large for use in the standard proof
-  procedures, but {\tt slow_step_tac} is worth considering in special
-  situations.
+  The resulting search space is larger.
 \end{ttdescription}