--- a/doc-src/HOL/logics-HOL.tex Wed Mar 06 14:48:21 2002 +0100
+++ b/doc-src/HOL/logics-HOL.tex Wed Mar 06 16:18:45 2002 +0100
@@ -44,10 +44,9 @@
\begin{abstract}
This manual describes Isabelle's formalization of Higher-Order Logic, a
polymorphic version of Church's Simple Theory of Types. HOL can be best
- understood as a simply-typed version of classical set theory. See also
- \emph{Isabelle/HOL --- The Tutorial} for a gentle introduction on using
- Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle
- commands.
+ understood as a simply-typed version of classical set theory. The monograph
+ \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
+ gentle introduction on using Isabelle/HOL in practice.
\end{abstract}
\pagenumbering{roman} \tableofcontents \clearfirst