# HG changeset patch
# User paulson
# Date 951298897 -3600
# Node ID 95c022a866ca4c207a8b65124ad1f7e403b2f411
# Parent  0a319c5746eb218fca219a54067381c11115234b
new reference korf85

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.
   
diff -r 0a319c5746eb -r 95c022a866ca doc-src/manual.bib
--- a/doc-src/manual.bib	Tue Feb 22 21:53:17 2000 +0100
+++ b/doc-src/manual.bib	Wed Feb 23 10:41:37 2000 +0100
@@ -18,6 +18,7 @@
 @string{Edinburgh="Dept. Comp. Sci., Univ. Edinburgh"}
 
 %journals
+@string{AI="Artificial Intelligence"}
 @string{FAC="Formal Aspects Comput."}
 @string{JAR="J. Auto. Reas."}
 @string{JCS="J. Comput. Secur."}
@@ -390,9 +391,20 @@
   title = 	 {Locales: A Sectioning Concept for {Isabelle}},
   crossref =	 {tphols99}}
 
-@book{Knuth3-75,author={Donald E. Knuth},
-title={The Art of Computer Programming, Volume 3: Sorting and Searching},
-publisher={Addison-Wesley},year=1975}
+@book{Knuth3-75,
+  author={Donald E. Knuth},
+  title={The Art of Computer Programming, Volume 3: Sorting and Searching},
+  publisher={Addison-Wesley},
+  year=1975}
+
+@Article{korf85,
+  author	= {R. E. Korf},
+  title		= {Depth-First Iterative-Deepening: an Optimal Admissible
+		 Tree Search},
+  journal	= AI,
+  year		= 1985,
+  volume	= 27,
+  pages		= {97-109}}
 
 @Book{kunen80,
   author	= {Kenneth Kunen},