# HG changeset patch
# User wenzelm
# Date 881943781 -3600
# Node ID 6c5d61fd337953a1d166054b83c7950da8dc6aec
# Parent  7f760385a3a5c4981fb36f0be552d0722b298660
tuned;

diff -r 7f760385a3a5 -r 6c5d61fd3379 doc-src/Ref/classical.tex
--- 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.