--- 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.
--- 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},