doc-src/Ref/classical.tex

--- a/doc-src/Ref/classical.tex	Sat Jun 11 15:36:46 2011 +0200
+++ b/doc-src/Ref/classical.tex	Sat Jun 11 16:05:17 2011 +0200
@@ -136,28 +136,6 @@
 \end{ttdescription}
 
 
-\subsection{Depth-limited automatic 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 \texttt{fast_tac} can but 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 prove subgoal~$i$ by exhaustive search up to depth~$m$.
-
-\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
-tries to prove subgoal~$i$ by iterative deepening.  It calls \texttt{depth_tac}
-repeatedly with increasing depths, starting with~$m$.
-\end{ttdescription}
-
-
 \subsection{Other useful tactics}
 \index{tactics!for contradiction}
 \index{tactics!for Modus Ponens}