tidying, e.g. from \\tt to \\texttt
authorpaulson
Mon Jan 11 10:22:04 1999 +0100 (1999-01-11)
changeset 6076560396301672
parent 6075 c148037f53c6
child 6077 60d97d521453
tidying, e.g. from \\tt to \\texttt
doc-src/Logics/HOL.tex
     1.1 --- a/doc-src/Logics/HOL.tex	Sat Jan 09 17:55:54 1999 +0100
     1.2 +++ b/doc-src/Logics/HOL.tex	Mon Jan 11 10:22:04 1999 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4  denote something, a description is always meaningful, but we do not
     1.5  know its value unless $P$ defines it uniquely.  We may write
     1.6  descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
     1.7 -\hbox{\tt \at $x$. $P[x]$}.
     1.8 +\hbox{\tt \at $x$.\ $P[x]$}.
     1.9  
    1.10  Existential quantification is defined by
    1.11  \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
    1.12 @@ -222,7 +222,7 @@
    1.13  available.  Both notations are accepted for input.  The {\ML} reference
    1.14  \ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
    1.15  true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
    1.16 -to \texttt{false}, then~{\tt ALL} and~{\tt EX} are displayed.
    1.17 +to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed.
    1.18  
    1.19  If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
    1.20  variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
    1.21 @@ -253,7 +253,7 @@
    1.22  as a uniform means of expressing \texttt{case} constructs.  Therefore \texttt{case}
    1.23  and \sdx{of} are reserved words.  Initially, this is mere syntax and has no
    1.24  logical meaning.  By declaring translations, you can cause instances of the
    1.25 -{\tt case} construct to denote applications of particular case operators.
    1.26 +\texttt{case} construct to denote applications of particular case operators.
    1.27  This is what happens automatically for each \texttt{datatype} definition
    1.28  (see~\S\ref{sec:HOL:datatype}).
    1.29  
    1.30 @@ -590,13 +590,13 @@
    1.31  $\neg(a\in b)$.  
    1.32  
    1.33  The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
    1.34 -the obvious manner using~{\tt insert} and~$\{\}$:
    1.35 +the obvious manner using~\texttt{insert} and~$\{\}$:
    1.36  \begin{eqnarray*}
    1.37    \{a, b, c\} & \equiv &
    1.38    \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
    1.39  \end{eqnarray*}
    1.40  
    1.41 -The set \hbox{\tt{\ttlbrace}$x$. $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
    1.42 +The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
    1.43  that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
    1.44  occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
    1.45  x. P[x])$.  It defines sets by absolute comprehension, which is impossible
    1.46 @@ -612,19 +612,19 @@
    1.47  write\index{*"! symbol}\index{*"? symbol}
    1.48  \index{*ALL symbol}\index{*EX symbol} 
    1.49  %
    1.50 -\hbox{\tt !~$x$:$A$. $P[x]$} and \hbox{\tt ?~$x$:$A$. $P[x]$}.  Isabelle's
    1.51 +\hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}.  Isabelle's
    1.52  usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
    1.53  for input.  As with the primitive quantifiers, the {\ML} reference
    1.54  \ttindex{HOL_quantifiers} specifies which notation to use for output.
    1.55  
    1.56  Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
    1.57  $\bigcap@{x\in A}B[x]$, are written 
    1.58 -\sdx{UN}~\hbox{\tt$x$:$A$. $B[x]$} and
    1.59 -\sdx{INT}~\hbox{\tt$x$:$A$. $B[x]$}.  
    1.60 +\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and
    1.61 +\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.  
    1.62  
    1.63  Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
    1.64 -B[x]$, are written \sdx{UN}~\hbox{\tt$x$. $B[x]$} and
    1.65 -\sdx{INT}~\hbox{\tt$x$. $B[x]$}.  They are equivalent to the previous
    1.66 +B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and
    1.67 +\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}.  They are equivalent to the previous
    1.68  union and intersection operators when $A$ is the universal set.
    1.69  
    1.70  The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are
    1.71 @@ -905,9 +905,8 @@
    1.72  
    1.73  \subsection{Simplification and substitution}
    1.74  
    1.75 -Simplification tactics tactics such as {\tt
    1.76 -  Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
    1.77 -({\tt simpset()}), which works for most purposes.  A quite minimal
    1.78 +Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
    1.79 +(\texttt{simpset()}), which works for most purposes.  A quite minimal
    1.80  simplification set for higher-order logic is~\ttindexbold{HOL_ss};
    1.81  even more frugal is \ttindexbold{HOL_basic_ss}.  Equality~($=$), which
    1.82  also expresses logical equivalence, may be used for rewriting.  See
    1.83 @@ -946,7 +945,7 @@
    1.84  \label{subsec:HOL:case:splitting}
    1.85  
    1.86  \HOL{} also provides convenient means for case splitting during
    1.87 -rewriting. Goals containing a subterm of the form {\tt if}~$b$~{\tt
    1.88 +rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
    1.89  then\dots else\dots} often require a case distinction on $b$. This is
    1.90  expressed by the theorem \tdx{split_if}:
    1.91  $$
    1.92 @@ -1006,7 +1005,7 @@
    1.93  rule; recall Fig.\ts\ref{hol-lemmas2} above.
    1.94  
    1.95  The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
    1.96 -Best_tac} refer to the default claset ({\tt claset()}), which works for most
    1.97 +Best_tac} refer to the default claset (\texttt{claset()}), which works for most
    1.98  purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
    1.99  propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier
   1.100  rules.  See the file \texttt{HOL/cladata.ML} for lists of the classical rules,
   1.101 @@ -1076,12 +1075,12 @@
   1.102  In addition, it is possible to use tuples
   1.103  as patterns in abstractions:
   1.104  \begin{center}
   1.105 -{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$. $t$)} 
   1.106 +{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} 
   1.107  \end{center}
   1.108  Nested patterns are also supported.  They are translated stepwise:
   1.109  {\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$
   1.110  {\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$
   1.111 -  $z$. $t$))}.  The reverse translation is performed upon printing.
   1.112 +  $z$.\ $t$))}.  The reverse translation is performed upon printing.
   1.113  \begin{warn}
   1.114    The translation between patterns and \texttt{split} is performed automatically
   1.115    by the parser and printer.  Thus the internal and external form of a term
   1.116 @@ -1273,8 +1272,8 @@
   1.117  Reasoning about arithmetic inequalities can be tedious.  A minimal amount of
   1.118  automation is provided by the tactic \ttindex{trans_tac} of type \texttt{int ->
   1.119  tactic} that deals with simple inequalities.  Note that it only knows about
   1.120 -{\tt 0}, \texttt{Suc}, {\tt<} and {\tt<=}.  The following goals are all solved by
   1.121 -{\tt trans_tac 1}:
   1.122 +\texttt{0}, \texttt{Suc}, {\tt<} and {\tt<=}.  The following goals are all solved by
   1.123 +\texttt{trans_tac 1}:
   1.124  \begin{ttbox}
   1.125  {\out  1. \dots ==> m <= Suc(Suc m)}
   1.126  {\out  1. [| \dots i <= j \dots Suc j <= k \dots |] ==> i < k}
   1.127 @@ -1425,7 +1424,7 @@
   1.128  which can be fed to \ttindex{addsplits} just like
   1.129  \texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}).
   1.130  
   1.131 -{\tt List} provides a basic library of list processing functions defined by
   1.132 +\texttt{List} provides a basic library of list processing functions defined by
   1.133  primitive recursion (see~\S\ref{sec:HOL:primrec}).  The recursion equations
   1.134  are shown in Fig.\ts\ref{fig:HOL:list-simps}.
   1.135  
   1.136 @@ -1784,7 +1783,7 @@
   1.137  \label{sec:HOL:datatype}
   1.138  \index{*datatype|(}
   1.139  
   1.140 -Inductive datatypes, similar to those of \ML, frequently appear in actual
   1.141 +Inductive datatypes, similar to those of \ML, frequently appear in 
   1.142  applications of Isabelle/HOL.  In principle, such types could be defined by
   1.143  hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
   1.144  tedious.  The \ttindex{datatype} definition package of \HOL\ automates such
   1.145 @@ -1832,12 +1831,12 @@
   1.146  (\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t'
   1.147  \]
   1.148  this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
   1.149 -example of a datatype is the type {\tt list}, which can be defined by
   1.150 +example of a datatype is the type \texttt{list}, which can be defined by
   1.151  \begin{ttbox}
   1.152  datatype 'a list = Nil
   1.153                   | Cons 'a ('a list)
   1.154  \end{ttbox}
   1.155 -Arithmetic expressions {\tt aexp} and boolean expressions {\tt bexp} can be modelled
   1.156 +Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled
   1.157  by the mutually recursive datatype definition
   1.158  \begin{ttbox}
   1.159  datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
   1.160 @@ -1849,7 +1848,7 @@
   1.161                   | And ('a bexp) ('a bexp)
   1.162                   | Or ('a bexp) ('a bexp)
   1.163  \end{ttbox}
   1.164 -The datatype {\tt term}, which is defined by
   1.165 +The datatype \texttt{term}, which is defined by
   1.166  \begin{ttbox}
   1.167  datatype ('a, 'b) term = Var 'a
   1.168                         | App 'b ((('a, 'b) term) list)
   1.169 @@ -1869,7 +1868,7 @@
   1.170  must have a constructor $C^j@i$ without recursive arguments, a \emph{base
   1.171    case}, to ensure that the new types are non-empty. If there are nested
   1.172  occurrences, a datatype can even be non-empty without having a base case
   1.173 -itself. Since {\tt list} is a non-empty datatype, {\tt datatype t = C (t
   1.174 +itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
   1.175    list)} is non-empty as well.
   1.176  
   1.177  The datatype constructors are automatically defined as functions of their
   1.178 @@ -1935,7 +1934,7 @@
   1.179  \]
   1.180  i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
   1.181  
   1.182 -For datatypes with nested recursion, such as the {\tt term} example from
   1.183 +For datatypes with nested recursion, such as the \texttt{term} example from
   1.184  above, things are a bit more complicated.  Conceptually, Isabelle/HOL unfolds
   1.185  a definition like
   1.186  \begin{ttbox}
   1.187 @@ -1949,11 +1948,11 @@
   1.188  and      ('a, 'b) term_list = Nil'
   1.189                              | Cons' (('a,'b) term) (('a,'b) term_list)
   1.190  \end{ttbox}
   1.191 -Note however, that the type {\tt ('a,'b) term_list} and the constructors {\tt
   1.192 -  Nil'} and {\tt Cons'} are not really introduced.  One can directly work with
   1.193 -the original (isomorphic) type {\tt (('a, 'b) term) list} and its existing
   1.194 -constructors {\tt Nil} and {\tt Cons}. Thus, the structural induction rule for
   1.195 -{\tt term} gets the form
   1.196 +Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
   1.197 +  Nil'} and \texttt{Cons'} are not really introduced.  One can directly work with
   1.198 +the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
   1.199 +constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
   1.200 +\texttt{term} gets the form
   1.201  \[
   1.202  \infer{P@1~x@1 \wedge P@2~x@2}
   1.203    {\begin{array}{l}
   1.204 @@ -1963,11 +1962,11 @@
   1.205       \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)
   1.206     \end{array}}
   1.207  \]
   1.208 -Note that there are two predicates $P@1$ and $P@2$, one for the type {\tt ('a,'b) term}
   1.209 -and one for the type {\tt (('a, 'b) term) list}.
   1.210 +Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
   1.211 +and one for the type \texttt{(('a, 'b) term) list}.
   1.212  
   1.213  \medskip In principle, inductive types are already fully determined by
   1.214 -freeness and structural induction.  For convenience in actual applications,
   1.215 +freeness and structural induction.  For convenience in applications,
   1.216  the following derived constructions are automatically provided for any
   1.217  datatype.
   1.218  
   1.219 @@ -2065,8 +2064,8 @@
   1.220    {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous
   1.221    structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$.  This
   1.222    is the canonical way to prove properties of mutually recursive datatypes
   1.223 -  such as {\tt aexp} and {\tt bexp}, or datatypes with nested recursion such as
   1.224 -  {\tt term}.
   1.225 +  such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as
   1.226 +  \texttt{term}.
   1.227  \end{ttdescription}
   1.228  In some cases, induction is overkill and a case distinction over all
   1.229  constructors of the datatype suffices.
   1.230 @@ -2101,22 +2100,22 @@
   1.231  val size : thm list
   1.232  val simps : thm list
   1.233  \end{ttbox}
   1.234 -{\tt distinct}, \texttt{inject}, \texttt{induct}, {\tt size}
   1.235 -and {\tt split} contain the theorems
   1.236 +\texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}
   1.237 +and \texttt{split} contain the theorems
   1.238  described above.  For user convenience, \texttt{distinct} contains
   1.239  inequalities in both directions.  The reduction rules of the {\tt
   1.240    case}-construct are in \texttt{cases}.  All theorems from {\tt
   1.241    distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.
   1.242 -In case of mutually recursive datatypes, {\tt recs}, {\tt size}, {\tt induct}
   1.243 -and {\tt simps} are contained in a separate structure named $t@1_\ldots_t@n$.
   1.244 +In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
   1.245 +and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
   1.246  
   1.247  
   1.248  \subsection{Representing existing types as datatypes}
   1.249  
   1.250 -For foundational reasons, some basic types such as {\tt nat}, {\tt *}, {\tt
   1.251 -  +}, {\tt bool} and {\tt unit} are not defined in a {\tt datatype} section,
   1.252 +For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
   1.253 +  +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
   1.254  but by more primitive means using \texttt{typedef}. To be able to use the
   1.255 -tactics {\tt induct_tac} and {\tt exhaust_tac} and to define functions by
   1.256 +tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by
   1.257  primitive recursion on these types, such types may be represented as actual
   1.258  datatypes.  This is done by specifying an induction rule, as well as theorems
   1.259  stating the distinctness and injectivity of constructors in a {\tt
   1.260 @@ -2338,8 +2337,8 @@
   1.261  \end{ttbox}
   1.262  
   1.263  \subsubsection{Example: Evaluation of expressions}
   1.264 -Using mutual primitive recursion, we can define evaluation functions {\tt eval_aexp}
   1.265 -and {\tt eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
   1.266 +Using mutual primitive recursion, we can define evaluation functions \texttt{eval_aexp}
   1.267 +and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
   1.268  \S\ref{subsec:datatype:basics}:
   1.269  \begin{ttbox}
   1.270  consts
   1.271 @@ -2359,13 +2358,13 @@
   1.272    "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
   1.273  \end{ttbox}
   1.274  Since the value of an expression depends on the value of its variables,
   1.275 -the functions {\tt eval_aexp} and {\tt eval_bexp} take an additional
   1.276 -parameter, an {\em environment} of type {\tt 'a => nat}, which maps
   1.277 +the functions \texttt{eval_aexp} and \texttt{eval_bexp} take an additional
   1.278 +parameter, an {\em environment} of type \texttt{'a => nat}, which maps
   1.279  variables to their values.
   1.280  
   1.281 -Similarly, we may define substitution functions {\tt subst_aexp}
   1.282 -and {\tt subst_bexp} for expressions: The mapping {\tt f} of type
   1.283 -{\tt 'a => 'a aexp} given as a parameter is lifted canonically
   1.284 +Similarly, we may define substitution functions \texttt{subst_aexp}
   1.285 +and \texttt{subst_bexp} for expressions: The mapping \texttt{f} of type
   1.286 +\texttt{'a => 'a aexp} given as a parameter is lifted canonically
   1.287  on the types {'a aexp} and {'a bexp}:
   1.288  \begin{ttbox}
   1.289  consts
   1.290 @@ -2400,10 +2399,10 @@
   1.291  
   1.292  \subsubsection{Example: A substitution function for terms}
   1.293  Functions on datatypes with nested recursion, such as the type
   1.294 -{\tt term} mentioned in \S\ref{subsec:datatype:basics}, are
   1.295 +\texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are
   1.296  also defined by mutual primitive recursion. A substitution
   1.297 -function {\tt subst_term} on type {\tt term}, similar to the functions
   1.298 -{\tt subst_aexp} and {\tt subst_bexp} described above, can
   1.299 +function \texttt{subst_term} on type \texttt{term}, similar to the functions
   1.300 +\texttt{subst_aexp} and \texttt{subst_bexp} described above, can
   1.301  be defined as follows:
   1.302  \begin{ttbox}
   1.303  consts
   1.304 @@ -2420,7 +2419,7 @@
   1.305       subst_term f t # subst_term_list f ts"
   1.306  \end{ttbox}
   1.307  The recursion scheme follows the structure of the unfolded definition of type
   1.308 -{\tt term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
   1.309 +\texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
   1.310  this substitution function, mutual induction is needed:
   1.311  \begin{ttbox}
   1.312  Goal
   1.313 @@ -2653,7 +2652,7 @@
   1.314  
   1.315  \item[\tt elims] is the list of elimination rule.
   1.316  
   1.317 -\item[\tt elim] is the head of the list {\tt elims}.
   1.318 +\item[\tt elim] is the head of the list \texttt{elims}.
   1.319    
   1.320  \item[\tt mk_cases] is a function to create simplified instances of {\tt
   1.321  elim}, using freeness reasoning on some underlying datatype.
   1.322 @@ -2695,7 +2694,7 @@
   1.323    con_defs   {\it constructor definitions}
   1.324  \end{ttbox}
   1.325  A coinductive definition is identical, except that it starts with the keyword
   1.326 -{\tt coinductive}.  
   1.327 +\texttt{coinductive}.  
   1.328  
   1.329  The \texttt{monos} and \texttt{con_defs} sections are optional.  If present,
   1.330  each is specified by a list of identifiers.
   1.331 @@ -2719,7 +2718,7 @@
   1.332  
   1.333  \subsection{Example of an inductive definition}
   1.334  Two declarations, included in a theory file, define the finite powerset
   1.335 -operator.  First we declare the constant~{\tt Fin}.  Then we declare it
   1.336 +operator.  First we declare the constant~\texttt{Fin}.  Then we declare it
   1.337  inductively, with two introduction rules:
   1.338  \begin{ttbox}
   1.339  consts Fin :: 'a set => 'a set set
   1.340 @@ -2728,13 +2727,13 @@
   1.341      emptyI  "{\ttlbrace}{\ttrbrace} : Fin A"
   1.342      insertI "[| a: A;  b: Fin A |] ==> insert a b : Fin A"
   1.343  \end{ttbox}
   1.344 -The resulting theory structure contains a substructure, called~{\tt Fin}.
   1.345 +The resulting theory structure contains a substructure, called~\texttt{Fin}.
   1.346  It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
   1.347  and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}.  The induction
   1.348  rule is \texttt{Fin.induct}.
   1.349  
   1.350  For another example, here is a theory file defining the accessible
   1.351 -part of a relation.  The main thing to note is the use of~{\tt Pow} in
   1.352 +part of a relation.  The main thing to note is the use of~\texttt{Pow} in
   1.353  the sole introduction rule, and the corresponding mention of the rule
   1.354  \verb|Pow_mono| in the \texttt{monos} list.  The paper
   1.355  \cite{paulson-CADE} discusses a \ZF\ version of this example in more
   1.356 @@ -2753,7 +2752,7 @@
   1.357  The Isabelle distribution contains many other inductive definitions.  Simple
   1.358  examples are collected on subdirectory \texttt{HOL/Induct}.  The theory
   1.359  \texttt{HOL/Induct/LList} contains coinductive definitions.  Larger examples
   1.360 -may be found on other subdirectories of \texttt{HOL}, such as {\tt IMP},
   1.361 +may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP},
   1.362  \texttt{Lambda} and \texttt{Auth}.
   1.363  
   1.364  \index{*coinductive|)} \index{*inductive|)}
   1.365 @@ -2802,7 +2801,7 @@
   1.366    set of theorems defined inductively.  A similar proof in \ZF{} is
   1.367    described elsewhere~\cite{paulson-set-II}.
   1.368  
   1.369 -\item Theory \texttt{Term} defines the datatype {\tt term}.
   1.370 +\item Theory \texttt{Term} defines the datatype \texttt{term}.
   1.371  
   1.372  \item Theory \texttt{ABexp} defines arithmetic and boolean expressions
   1.373   as mutually recursive datatypes.
   1.374 @@ -2951,7 +2950,7 @@
   1.375  {\out No subgoals!}
   1.376  \end{ttbox}
   1.377  How much creativity is required?  As it happens, Isabelle can prove this
   1.378 -theorem automatically.  The default classical set {\tt claset()} contains rules
   1.379 +theorem automatically.  The default classical set \texttt{claset()} contains rules
   1.380  for most of the constructs of \HOL's set theory.  We must augment it with
   1.381  \tdx{equalityCE} to break up set equalities, and then apply best-first
   1.382  search.  Depth-first search would diverge, but best-first search