diff -r f4fe75218cec -r 0260bdba4dd7 src/Doc/Logics/document/preface.tex --- 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