diff -r ddf235f2384a -r 81c87faed78b doc-src/HOL/logics-HOL.tex
--- 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