--- a/src/Doc/Logics/document/preface.tex Sun Jul 07 18:50:16 2013 +0200
+++ b/src/Doc/Logics/document/preface.tex Sun Jul 07 20:23:09 2013 +0200
@@ -8,8 +8,7 @@
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.
+applications.
\texttt{ZF} provides another starting point for applications, with a slightly
less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages