1.1 --- a/doc-src/Ref/classical.tex	Tue Feb 22 21:53:17 2000 +0100
     1.2 +++ b/doc-src/Ref/classical.tex	Wed Feb 23 10:41:37 2000 +0100
     1.3 @@ -470,10 +470,11 @@
     1.4  successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
     1.5  \begin{ttdescription}
     1.6  \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
     1.7 -  subgoal~$i$ using iterative deepening to increase the search bound.
     1.8 +  subgoal~$i$, increasing the search bound using iterative
     1.9 +  deepening~\cite{korf85}. 
    1.10    
    1.11  \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
    1.12 -  to prove subgoal~$i$ using a search bound of $lim$.  Often a slow
    1.13 +  to prove subgoal~$i$ using a search bound of $lim$.  Sometimes a slow
    1.14    proof using \texttt{blast_tac} can be made much faster by supplying the
    1.15    successful search bound to this tactic instead.
    1.16    

     2.1 --- a/doc-src/manual.bib	Tue Feb 22 21:53:17 2000 +0100
     2.2 +++ b/doc-src/manual.bib	Wed Feb 23 10:41:37 2000 +0100
     2.3 @@ -18,6 +18,7 @@
     2.4  @string{Edinburgh="Dept. Comp. Sci., Univ. Edinburgh"}
     2.5  
     2.6  %journals
     2.7 +@string{AI="Artificial Intelligence"}
     2.8  @string{FAC="Formal Aspects Comput."}
     2.9  @string{JAR="J. Auto. Reas."}
    2.10  @string{JCS="J. Comput. Secur."}
    2.11 @@ -390,9 +391,20 @@
    2.12    title = 	 {Locales: A Sectioning Concept for {Isabelle}},
    2.13    crossref =	 {tphols99}}
    2.14  
    2.15 -@book{Knuth3-75,author={Donald E. Knuth},
    2.16 -title={The Art of Computer Programming, Volume 3: Sorting and Searching},
    2.17 -publisher={Addison-Wesley},year=1975}
    2.18 +@book{Knuth3-75,
    2.19 +  author={Donald E. Knuth},
    2.20 +  title={The Art of Computer Programming, Volume 3: Sorting and Searching},
    2.21 +  publisher={Addison-Wesley},
    2.22 +  year=1975}
    2.23 +
    2.24 +@Article{korf85,
    2.25 +  author	= {R. E. Korf},
    2.26 +  title		= {Depth-First Iterative-Deepening: an Optimal Admissible
    2.27 +		 Tree Search},
    2.28 +  journal	= AI,
    2.29 +  year		= 1985,
    2.30 +  volume	= 27,
    2.31 +  pages		= {97-109}}
    2.32  
    2.33  @Book{kunen80,
    2.34    author	= {Kenneth Kunen},