doc-src/Logics/CHOL.tex

 %% $Id$
 \chapter{Higher-Order Logic}
 \index{higher-order logic|(}
-\index{CHOL system@{\sc chol} system}
-
-The theory~\thydx{CHOL} implements higher-order logic with curried
-function application.  It is based on Gordon's~{\sc hol}
-system~\cite{mgordon-hol}, which itself is based on Church's original
-paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a full
-description of higher-order logic.  Experience with the {\sc hol}
-system has demonstrated that higher-order logic is useful for hardware
-verification; beyond this, it is widely applicable in many areas of
-mathematics.  It is weaker than {\ZF} set theory but for most
-applications this does not matter.  If you prefer {\ML} to Lisp, you
-will probably prefer \CHOL\ to~{\ZF}.
-
-\CHOL\ is a modified version of Isabelle's \HOL\ and uses curried function
-application. Therefore the expression $f(a,b)$ (which in \HOL\ means
-``f applied to the two arguments $a$ and $b$'') means ``f applied to
-the pair $(a,b)$'' in \CHOL. N.B. that ordered pairs in \HOL\ are written as
-$<a,b>$ while in \CHOL\ the syntax $(a,b)$ is used.  Previous
-releases of Isabelle also included a different version of~\HOL, with
-explicit type inference rules~\cite{paulson-COLOG}.  This version no
-longer exists, but \thydx{ZF} supports a similar style of reasoning.
-
-\CHOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
+\index{HOL system@{\sc chol} system}
+
+The theory~\thydx{HOL} implements higher-order logic.  It is based on
+Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
+Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a
+full description of higher-order logic.  Experience with the {\sc hol} system
+has demonstrated that higher-order logic is useful for hardware verification;
+beyond this, it is widely applicable in many areas of mathematics.  It is
+weaker than {\ZF} set theory but for most applications this does not matter.
+If you prefer {\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.
+
+The syntax of Isabelle's \HOL\ has recently been changed to look more like the
+traditional syntax of higher-order logic.  Function application is now
+curried.  To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you
+must write $f\,a\,b$.  Note that $f(a,b)$ means ``$f$ applied to the pair
+$(a,b)$'' in \HOL.  We write ordered pairs as $(a,b)$, not $\langle
+a,b\rangle$ as in {\ZF} and earlier versions of \HOL.  Early releases of
+Isabelle included still another version of~\HOL, with explicit type inference
+rules~\cite{paulson-COLOG}.  This version no longer exists, but \thydx{ZF}
+supports a similar style of reasoning.
+
+\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
 identifies object-level types with meta-level types, taking advantage of
 Isabelle's built-in type checker.  It identifies object-level functions
 with meta-level functions, so it uses Isabelle's operations for abstraction
 and application.  There is no `apply' operator: function applications are
 written as simply~$f~a$ rather than $f{\tt`}a$.
 
-These identifications allow Isabelle to support \CHOL\ particularly nicely,
-but they also mean that \CHOL\ requires more sophistication from the user
+These identifications allow Isabelle to support \HOL\ particularly nicely,
+but they also mean that \HOL\ requires more sophistication from the user
 --- in particular, an understanding of Isabelle's type system.  Beginners
 should work with {\tt show_types} set to {\tt true}.  Gain experience by
 working in first-order logic before attempting to use higher-order logic.
 This chapter assumes familiarity with~{\FOL{}}.
 

          & | & "EX~~" id~id^* " . " formula \\
          & | & "?!~~" id~id^* " . " formula 
          & | & "EX!~" id~id^* " . " formula
   \end{array}
 \]
-\caption{Full grammar for \CHOL} \label{chol-grammar}
+\caption{Full grammar for \HOL} \label{chol-grammar}
 \end{figure} 
 
 
 \section{Syntax}
 The type class of higher-order terms is called~\cldx{term}.  Type variables

 binders), while Fig.\ts\ref{chol-grammar} presents the grammar of
 higher-order logic.  Note that $a$\verb|~=|$b$ is translated to
 $\neg(a=b)$.
 
 \begin{warn}
-  \CHOL\ has no if-and-only-if connective; logical equivalence is expressed
+  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
   using equality.  But equality has a high priority, as befitting a
   relation, while if-and-only-if typically has the lowest priority.  Thus,
   $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
   When using $=$ to mean logical equivalence, enclose both operands in
   parentheses.
 \end{warn}
 
-\subsection{Types}\label{CHOL-types}
+\subsection{Types}\label{HOL-types}
 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
 formulae are terms.  The built-in type~\tydx{fun}, which constructs function
 types, is overloaded with arity {\tt(term,term)term}.  Thus, $\sigma\To\tau$
 belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
 over functions.
 
-Types in \CHOL\ must be non-empty; otherwise the quantifier rules would be
+Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
 unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
 
 \index{type definitions}
 Gordon's {\sc hol} system supports {\bf type definitions}.  A type is
 defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To

 Isabelle cannot enforce this.
 
 
 \subsection{Binders}
 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
-satisfying~$P[a]$, if such exists.  Since all terms in \CHOL\ denote
+satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
 something, a description is always meaningful, but we do not know its value
 unless $P[x]$ defines it uniquely.  We may write descriptions as
 \cdx{Eps}($P$) or use the syntax
 \hbox{\tt \at $x$.$P[x]$}.
 

 of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
 quantifications.  For instance, $\exists!x y.P~x~y$ abbreviates
 $\exists!x. \exists!y.P~x~y$; note that this does not mean that there
 exists a unique pair $(x,y)$ satisfying~$P~x~y$.
 
-\index{*"! symbol}\index{*"? symbol}\index{CHOL system@{\sc hol} system}
-Quantifiers have two notations.  As in Gordon's {\sc hol} system, \CHOL\
+\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
+Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
 existential quantifier must be followed by a space; thus {\tt?x} is an
 unknown, while \verb'? x.f x=y' is a quantification.  Isabelle's usual
 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
 available.  Both notations are accepted for input.  The {\ML} reference

 Local abbreviations can be introduced by a {\tt let} construct whose
 syntax appears in Fig.\ts\ref{chol-grammar}.  Internally it is translated into
 the constant~\cdx{Let}.  It can be expanded by rewriting with its
 definition, \tdx{Let_def}.
 
-\CHOL\ also defines the basic syntax
+\HOL\ also defines the basic syntax
 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
 as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
   case} and \sdx{of} are reserved words.  However, so far this is mere
 syntax and has no logical meaning.  By declaring translations, you can
 cause instances of the {\tt case} construct to denote applications of

 \tdx{mp}             [| P-->Q;  P |] ==> Q
 \tdx{iff}            (P-->Q) --> (Q-->P) --> (P=Q)
 \tdx{selectI}        P(x::'a) ==> P(@x.P x)
 \tdx{True_or_False}  (P=True) | (P=False)
 \end{ttbox}
-\caption{The {\tt CHOL} rules} \label{chol-rules}
+\caption{The {\tt HOL} rules} \label{chol-rules}
 \end{figure}
 
 
 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
 \begin{ttbox}\makeatother

 \tdx{Inv_def}    Inv      == (\%(f::'a=>'b) y. @x. f x=y)
 \tdx{o_def}      op o     == (\%(f::'b=>'c) g (x::'a). f(g x))
 \tdx{if_def}     If P x y == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
 \tdx{Let_def}    Let s f  == f s
 \end{ttbox}
-\caption{The {\tt CHOL} definitions} \label{chol-defs}
+\caption{The {\tt HOL} definitions} \label{chol-defs}
 \end{figure}
 
 
 \section{Rules of inference}
-Figure~\ref{chol-rules} shows the inference rules of~\CHOL{}, with
+Figure~\ref{chol-rules} shows the inference rules of~\HOL{}, with
 their~{\ML} names.  Some of the rules deserve additional comments:
 \begin{ttdescription}
 \item[\tdx{ext}] expresses extensionality of functions.
 \item[\tdx{iff}] asserts that logically equivalent formulae are
   equal.

 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
     fact, the $\epsilon$-operator already makes the logic classical, as
     shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
 \end{ttdescription}
 
-\CHOL{} follows standard practice in higher-order logic: only a few
+\HOL{} follows standard practice in higher-order logic: only a few
 connectives are taken as primitive, with the remainder defined obscurely
 (Fig.\ts\ref{chol-defs}).  Gordon's {\sc hol} system expresses the
 corresponding definitions \cite[page~270]{mgordon-hol} using
 object-equality~({\tt=}), which is possible because equality in
 higher-order logic may equate formulae and even functions over formulae.
-But theory~\CHOL{}, like all other Isabelle theories, uses
+But theory~\HOL{}, like all other Isabelle theories, uses
 meta-equality~({\tt==}) for definitions.
 
 Some of the rules mention type variables; for example, {\tt refl}
 mentions the type variable~{\tt'a}.  This allows you to instantiate
 type variables explicitly by calling {\tt res_inst_tac}.  By default,

 \tdx{eqTrueI}     P ==> P=True 
 \tdx{eqTrueE}     P=True ==> P 
 \subcaption{Logical equivalence}
 
 \end{ttbox}
-\caption{Derived rules for \CHOL} \label{chol-lemmas1}
+\caption{Derived rules for \HOL} \label{chol-lemmas1}
 \end{figure}
 
 
 \begin{figure}
 \begin{ttbox}\makeatother

 may be defined by absolute comprehension.
 \item
 Although sets may contain other sets as elements, the containing set must
 have a more complex type.
 \end{itemize}
-Finite unions and intersections have the same behaviour in \CHOL\ as they
-do in~{\ZF}.  In \CHOL\ the intersection of the empty set is well-defined,
+Finite unions and intersections have the same behaviour in \HOL\ as they
+do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
 denoting the universal set for the given type.
 
 
 \subsection{Syntax of set theory}\index{*set type}
-\CHOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
+\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
 essentially the same as $\alpha\To bool$.  The new type is defined for
 clarity and to avoid complications involving function types in unification.
 Since Isabelle does not support type definitions (as mentioned in
-\S\ref{CHOL-types}), the isomorphisms between the two types are declared
+\S\ref{HOL-types}), the isomorphisms between the two types are declared
 explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
 $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
 argument order).
 
 Figure~\ref{chol-set-syntax} lists the constants, infixes, and syntax

 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
 are designed for classical reasoning; the rules \tdx{subsetD},
 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
 strictly necessary but yield more natural proofs.  Similarly,
 \tdx{equalityCE} supports classical reasoning about extensionality,
-after the fashion of \tdx{iffCE}.  See the file {\tt CHOL/Set.ML} for
+after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
 proofs pertaining to set theory.
 
 Figure~\ref{chol-fun} presents derived inference rules involving functions.
 They also include rules for \cdx{Inv}, which is defined in theory~{\tt
-  CHOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an
+  HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an
 inverse of~$f$.  They also include natural deduction rules for the image
 and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
 Reasoning about function composition (the operator~\sdx{o}) and the
 predicate~\cdx{surj} is done simply by expanding the definitions.  See
-the file {\tt CHOL/fun.ML} for a complete listing of the derived rules.
+the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
 
 Figure~\ref{chol-subset} presents lattice properties of the subset relation.
 Unions form least upper bounds; non-empty intersections form greatest lower
 bounds.  Reasoning directly about subsets often yields clearer proofs than
-reasoning about the membership relation.  See the file {\tt CHOL/subset.ML}.
+reasoning about the membership relation.  See the file {\tt HOL/subset.ML}.
 
 Figure~\ref{chol-equalities} presents many common set equalities.  They
 include commutative, associative and distributive laws involving unions,
 intersections and complements.  The proofs are mostly trivial, using the
-classical reasoner; see file {\tt CHOL/equalities.ML}.
+classical reasoner; see file {\tt HOL/equalities.ML}.
 
 
 \begin{figure}
 \begin{constants}
   \it symbol    & \it meta-type &           & \it description \\ 

 \caption{Type $\alpha+\beta$}\label{chol-sum}
 \end{figure}
 
 
 \section{Generic packages and classical reasoning}
-\CHOL\ instantiates most of Isabelle's generic packages;
-see {\tt CHOL/ROOT.ML} for details.
+\HOL\ instantiates most of Isabelle's generic packages;
+see {\tt HOL/ROOT.ML} for details.
 \begin{itemize}
 \item 
-Because it includes a general substitution rule, \CHOL\ instantiates the
+Because it includes a general substitution rule, \HOL\ instantiates the
 tactic {\tt hyp_subst_tac}, which substitutes for an equality
 throughout a subgoal and its hypotheses.
 \item 
 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
 simplification set for higher-order logic.  Equality~($=$), which also
 expresses logical equivalence, may be used for rewriting.  See the file
-{\tt CHOL/simpdata.ML} for a complete listing of the simplification
+{\tt HOL/simpdata.ML} for a complete listing of the simplification
 rules. 
 \item 
 It instantiates the classical reasoner, as described below. 
 \end{itemize}
-\CHOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
+\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
 rule; recall Fig.\ts\ref{chol-lemmas2} above.
 
 The classical reasoner is set up as the structure
 {\tt Classical}.  This structure is open, so {\ML} identifiers such

 Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
 overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
 Isabelle provides no means of verifying that such overloading is sensible;
 there is no means of specifying the operators' properties and verifying
 that instances of the operators satisfy those properties.  To be safe, the
-\CHOL\ theory includes no polymorphic axioms asserting general properties of
+\HOL\ theory includes no polymorphic axioms asserting general properties of
 $<$ and~$\leq$.
 
 Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
 defines addition, multiplication, subtraction, division, and remainder.
 Many of their properties are proved: commutative, associative and

 \end{figure}
 
 \begin{figure}
 \begin{ttbox}\makeatother
 \tdx{list_rec_Nil}    list_rec [] c h = c  
-\tdx{list_rec_Cons}   list_rec a#l c h = h a l (list_rec l c h)
+\tdx{list_rec_Cons}   list_rec (a#l) c h = h a l (list_rec l c h)
 
 \tdx{list_case_Nil}   list_case c h [] = c 
-\tdx{list_case_Cons}  list_case c h x#xs = h x xs
+\tdx{list_case_Cons}  list_case c h (x#xs) = h x xs
 
 \tdx{map_Nil}         map f [] = []
-\tdx{map_Cons}        map f x \# xs = f x \# map f xs
+\tdx{map_Cons}        map f (x#xs) = f x # map f xs
 
 \tdx{null_Nil}        null [] = True
-\tdx{null_Cons}       null x#xs = False
-
-\tdx{hd_Cons}         hd x#xs = x
-\tdx{tl_Cons}         tl x#xs = xs
+\tdx{null_Cons}       null (x#xs) = False
+
+\tdx{hd_Cons}         hd (x#xs) = x
+\tdx{tl_Cons}         tl (x#xs) = xs
 
 \tdx{ttl_Nil}         ttl [] = []
-\tdx{ttl_Cons}        ttl x#xs = xs
+\tdx{ttl_Cons}        ttl (x#xs) = xs
 
 \tdx{append_Nil}      [] @ ys = ys
 \tdx{append_Cons}     (x#xs) \at ys = x # xs \at ys
 
 \tdx{mem_Nil}         x mem [] = False
 \tdx{mem_Cons}        x mem (y#ys) = if y=x then True else x mem ys
 
 \tdx{filter_Nil}      filter P [] = []
-\tdx{filter_Cons}     filter P x#xs = if P x then x#filter P xs else filter P xs
+\tdx{filter_Cons}     filter P (x#xs) = if P x then x#filter P xs else filter P xs
 
 \tdx{list_all_Nil}    list_all P [] = True
-\tdx{list_all_Cons}   list_all P x#xs = (P x & list_all P xs)
+\tdx{list_all_Cons}   list_all P (x#xs) = (P x & list_all P xs)
 \end{ttbox}
 \caption{Rewrite rules for lists} \label{chol-list-simps}
 \end{figure}
 
 
 \subsection{The type constructor for lists, {\tt list}}
 \index{*list type}
 
-\CHOL's definition of lists is an example of an experimental method for
+\HOL's definition of lists is an example of an experimental method for
 handling recursive data types.  Figure~\ref{chol-list} presents the theory
 \thydx{List}: the basic list operations with their types and properties.
 
 The \sdx{case} construct is defined by the following translation:
 {\dquotes

 \subsection{Examples}
 
 \subsubsection{The datatype $\alpha~list$}
 
 We want to define the type $\alpha~list$.\footnote{Of course there is a list
-  type in CHOL already. This is only an example.} To do this we have to build
-a new theory that contains the type definition. We start from {\tt CHOL}.
-\begin{ttbox}
-MyList = CHOL +
+  type in HOL already. This is only an example.} To do this we have to build
+a new theory that contains the type definition. We start from {\tt HOL}.
+\begin{ttbox}
+MyList = HOL +
   datatype 'a list = Nil | Cons 'a ('a list)
 end
 \end{ttbox}
 After loading the theory (\verb$use_thy "MyList"$), we can prove
 $Cons~x~xs\neq xs$.  First we build a suitable simpset for the simplifier:

 In this example we define the type $\alpha~list$ again but this time we want
 to write {\tt []} instead of {\tt Nil} and we want to use the infix operator
 \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
 after the constructor declarations as follows:
 \begin{ttbox}
-MyList = CHOL +
+MyList = HOL +
   datatype 'a list = "[]" ("[]") 
                    | "#" 'a ('a list) (infixr 70)
 end
 \end{ttbox}
 Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The

 \begin{ttbox}
 Append = MyList +
 consts app :: "['a list,'a list] => 'a list"
 rules 
    app_Nil   "app [] ys = ys"
-   app_Cons  "app x#xs ys = x#app xs ys"
+   app_Cons  "app (x#xs) ys = x#app xs ys"
 end
 \end{ttbox}
 this carries with it the danger of accidentally asserting an inconsistency,
 as in \verb$app [] ys = us$. Therefore primitive recursive functions on
 datatypes can be defined with a special syntax:
 \begin{ttbox}
 Append = MyList +
 consts app :: "'['a list,'a list] => 'a list"
 primrec app MyList.list
    app_Nil   "app [] ys = ys"
-   app_Cons  "app x#xs ys = x#app xs ys"
+   app_Cons  "app (x#xs) ys = x#app xs ys"
 end
 \end{ttbox}
 The system will now check that the two rules \verb$app_Nil$ and
 \verb$app_Cons$ do indeed form a primitive recursive definition, thus
 ensuring that consistency is maintained. For example

 substructure of the main theory structure.
 
 This package is derived from the ZF one, described in a
 separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
   longer version is distributed with Isabelle.} which you should refer to
-in case of difficulties.  The package is simpler than ZF's, thanks to CHOL's
+in case of difficulties.  The package is simpler than ZF's, thanks to HOL's
 automatic type-checking.  The type of the (co)inductive determines the
 domain of the fixedpoint definition, and the package does not use inference
 rules for type-checking.
 
 

   intrs
      pred "pred a r: Pow(acc r) ==> a: acc r"
   monos   "[Pow_mono]"
 end
 \end{ttbox}
-The CHOL distribution contains many other inductive definitions, such as the
-theory {\tt CHOL/ex/PropLog.thy} and the directory {\tt CHOL/IMP}.  The
-theory {\tt CHOL/ex/LList.thy} contains coinductive definitions.
+The HOL distribution contains many other inductive definitions, such as the
+theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}.  The
+theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
 
 \index{*coinductive|)} \index{*inductive|)} \underscoreoff
 
 
 \section{The examples directories}
-Directory {\tt CHOL/Subst} contains Martin Coen's mechanisation of a theory of
+Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
 substitutions and unifiers.  It is based on Paulson's previous
 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
 theory~\cite{mw81}. 
 
-Directory {\tt CHOL/IMP} contains a mechanised version of a semantic
+Directory {\tt HOL/IMP} contains a mechanised version of a semantic
 equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the
 denotational and operational semantics of a simple while-language, then
 proves the two equivalent.  It contains several datatype and inductive
 definitions, and demonstrates their use.
 
-Directory {\tt CHOL/ex} contains other examples and experimental proofs in
-{\CHOL}.  Here is an overview of the more interesting files.
+Directory {\tt HOL/ex} contains other examples and experimental proofs in
+{\HOL}.  Here is an overview of the more interesting files.
 \begin{itemize}
 \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
   predicate calculus theorems, ranging from simple tautologies to
   moderately difficult problems involving equality and quantifiers.
 

 %
 Viewing types as sets, $\alpha\To bool$ represents the powerset
 of~$\alpha$.  This version states that for every function from $\alpha$ to
 its powerset, some subset is outside its range.  
 
-The Isabelle proof uses \CHOL's set theory, with the type $\alpha\,set$ and
+The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
 the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
 quantified variable so that we may inspect the subset found by the proof.
 \begin{ttbox}
 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
 {\out Level 0}

 {\out ~ \{x. ~ x : f x\} : range f}
 {\out No subgoals!}
 \end{ttbox}
 How much creativity is required?  As it happens, Isabelle can prove this
 theorem automatically.  The classical set \ttindex{set_cs} contains rules
-for most of the constructs of \CHOL's set theory.  We must augment it with
+for most of the constructs of \HOL's set theory.  We must augment it with
 \tdx{equalityCE} to break up set equalities, and then apply best-first
 search.  Depth-first search would diverge, but best-first search
 successfully navigates through the large search space.
 \index{search!best-first}
 \begin{ttbox}