diff -r 27d6e5d6a4a6 -r 75f31d45fb8b doc-src/Logics/preface.tex
--- a/doc-src/Logics/preface.tex	Tue May 04 18:04:45 1999 +0200
+++ b/doc-src/Logics/preface.tex	Tue May 04 18:05:34 1999 +0200
@@ -5,10 +5,21 @@
 starting points for defining new logics.  Each logic is distributed with
 sample proofs, some of which are described in this document.
 
-The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set
-theory) are described in a separate manual~\cite{isabelle-ZF}.  Here are the
-others:
+\texttt{HOL} is currently the best developed Isabelle object-logic, including
+an extensive library of (concrete) mathematics, and various packages for
+advanced definitional concepts (like (co-)inductive sets and types,
+well-founded recursion etc.). The distribution also includes some large
+applications.  See the separate manual \emph{Isabelle's Logics: HOL}.  There
+is also a comprehensive tutorial on Isabelle/HOL available.
 
+\texttt{ZF} provides another starting point for applications, with a slightly
+less developed library than \texttt{HOL}.  \texttt{ZF}'s definitional packages
+are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides
+more advanced constructions for sets than simply-typed \texttt{HOL}.
+\texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
+in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.
+
+\medskip There are some further logics distributed with Isabelle:
 \begin{ttdescription}
 \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
   which is the basis of a preliminary method for deriving programs from
@@ -17,14 +28,9 @@
 \item[\thydx{LCF}] is a version of Scott's Logic for Computable
   Functions, which is also implemented by the~{\sc lcf}
   system~\cite{paulson87}.  It is built upon classical~\FOL{}.
-
-\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
-which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
-This object-logic should not be confused with Isabelle's meta-logic, which is
-also a form of higher-order logic.
-
-\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an
-  extension of \texttt{HOL}\@.
+  
+\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
+  \texttt{HOL}\@. %FIXME See \cite{MNOS98} for more details on \texttt{HOLCF}.
  
 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
 Theory~\cite{nordstrom90}, with extensional equality.  Universes are not
@@ -44,19 +50,20 @@
 \item[\thydx{ILL}] implements intuitionistic linear logic.
 \end{ttdescription}
 
-The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt
-  Cube} are undocumented.  All object-logics' sources are
-distributed with Isabelle (see the directory \texttt{src}).  They are
-also available for browsing on the WWW at
+The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt
+  Cube} are undocumented.  All object-logics' sources are distributed with
+Isabelle (see the directory \texttt{src}).  They are also available for
+browsing on the WWW at
 \begin{ttbox}
 http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/
 http://isabelle.in.tum.de/library/
 \end{ttbox}
 Note that this is not necessarily consistent with your local sources!
 
-\medskip Do not read this manual before reading \emph{Introduction to
-  Isabelle} and performing some Isabelle proofs.  Consult the {\em Reference
-  Manual} for more information on tactics, packages, etc.
+\medskip Do not read the \emph{Isabelle's Logics} manuals before reading
+\emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and
+performing some Isabelle proofs.  Consult the {\em Reference Manual} for more
+information on tactics, packages, etc.
 
 
 %%% Local Variables: