diff -r 0a319c5746eb -r 95c022a866ca doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Tue Feb 22 21:53:17 2000 +0100
+++ b/doc-src/Ref/classical.tex	Wed Feb 23 10:41:37 2000 +0100
@@ -470,10 +470,11 @@
 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$ using iterative deepening to increase the search bound.
+  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$.  Often a slow
+  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.