1.1 --- a/doc-src/Ref/classical.tex	Fri Dec 12 17:14:58 1997 +0100
     1.2 +++ b/doc-src/Ref/classical.tex	Fri Dec 12 17:23:01 1997 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  Although Isabelle is generic, many users will be working in some
     1.6  extension of classical first-order logic.  Isabelle's set theory~{\tt
     1.7 -  ZF} is built upon theory~\texttt{FOL}, while higher-order logic
     1.8 +  ZF} is built upon theory~\texttt{FOL}, while {\HOL}
     1.9  conceptually contains first-order logic as a fragment.
    1.10  Theorem-proving in predicate logic is undecidable, but many
    1.11  researchers have developed strategies to assist in this task.