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