proper setup of iman.sty/extra.sty/ttbox.sty;
authorwenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695ec7d7f877712
parent 9694 13f3aaf12be2
child 9696 5c8acc0282c8
proper setup of iman.sty/extra.sty/ttbox.sty;
doc-src/HOL/HOL.tex
doc-src/HOL/Makefile
doc-src/HOL/logics-HOL.tex
doc-src/Inductive/Makefile
doc-src/Inductive/ind-defs.tex
doc-src/Intro/Makefile
doc-src/Intro/advanced.tex
doc-src/Intro/foundations.tex
doc-src/Intro/getting.tex
doc-src/Intro/intro.tex
doc-src/IsarRef/Makefile
doc-src/IsarRef/hol.tex
doc-src/IsarRef/isar-ref.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/refcard.tex
doc-src/Logics/CTT.tex
doc-src/Logics/LK.tex
doc-src/Logics/Makefile
doc-src/Logics/Old_HOL.tex
doc-src/Logics/logics.tex
doc-src/Logics/preface.tex
doc-src/Logics/syntax.tex
doc-src/Ref/Makefile
doc-src/Ref/classical.tex
doc-src/Ref/introduction.tex
doc-src/Ref/ref.tex
doc-src/Ref/simp.tex
doc-src/Ref/simplifier.tex
doc-src/Ref/substitution.tex
doc-src/Ref/syntax.tex
doc-src/Ref/tactic.tex
doc-src/Ref/theories.tex
doc-src/Ref/theory-syntax.tex
doc-src/System/Makefile
doc-src/System/fonts.tex
doc-src/System/present.tex
doc-src/System/system.tex
doc-src/Tutorial/Makefile
doc-src/Tutorial/extra.sty
doc-src/Tutorial/ttbox.sty
doc-src/Tutorial/tutorial.tex
doc-src/TutorialI/Makefile
doc-src/TutorialI/extra.sty
doc-src/TutorialI/ttbox.sty
doc-src/TutorialI/tutorial.tex
doc-src/ZF/FOL.tex
doc-src/ZF/Makefile
doc-src/ZF/ZF.tex
doc-src/ZF/logics-ZF.tex
     1.1 --- a/doc-src/HOL/HOL.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -5,41 +5,34 @@
     1.4  
     1.5  The theory~\thydx{HOL} implements higher-order logic.  It is based on
     1.6  Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
     1.7 -Church's original paper~\cite{church40}.  Andrews's
     1.8 -book~\cite{andrews86} is a full description of the original
     1.9 -Church-style higher-order logic.  Experience with the {\sc hol} system
    1.10 -has demonstrated that higher-order logic is widely applicable in many
    1.11 -areas of mathematics and computer science, not just hardware
    1.12 -verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}.  It is
    1.13 -weaker than {\ZF} set theory but for most applications this does not
    1.14 -matter.  If you prefer {\ML} to Lisp, you will probably prefer \HOL\ 
    1.15 -to~{\ZF}.
    1.16 -
    1.17 -The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
    1.18 -different syntax.  Ancient releases of Isabelle included still another version
    1.19 -of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}.  This
    1.20 -version no longer exists, but \thydx{ZF} supports a similar style of
    1.21 -reasoning.} follows $\lambda$-calculus and functional programming.  Function
    1.22 -application is curried.  To apply the function~$f$ of type
    1.23 -$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply
    1.24 -write $f\,a\,b$.  There is no `apply' operator as in \thydx{ZF}.  Note that
    1.25 -$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL.  We write ordered
    1.26 -pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.
    1.27 -
    1.28 -\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
    1.29 -identifies object-level types with meta-level types, taking advantage of
    1.30 -Isabelle's built-in type-checker.  It identifies object-level functions
    1.31 -with meta-level functions, so it uses Isabelle's operations for abstraction
    1.32 -and application.
    1.33 -
    1.34 -These identifications allow Isabelle to support \HOL\ particularly
    1.35 -nicely, but they also mean that \HOL\ requires more sophistication
    1.36 -from the user --- in particular, an understanding of Isabelle's type
    1.37 -system.  Beginners should work with \texttt{show_types} (or even
    1.38 -\texttt{show_sorts}) set to \texttt{true}.
    1.39 -%  Gain experience by
    1.40 -%working in first-order logic before attempting to use higher-order logic.
    1.41 -%This chapter assumes familiarity with~{\FOL{}}.
    1.42 +Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a
    1.43 +full description of the original Church-style higher-order logic.  Experience
    1.44 +with the {\sc hol} system has demonstrated that higher-order logic is widely
    1.45 +applicable in many areas of mathematics and computer science, not just
    1.46 +hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}.  It
    1.47 +is weaker than ZF set theory but for most applications this does not matter.
    1.48 +If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
    1.49 +
    1.50 +The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different
    1.51 +  syntax.  Ancient releases of Isabelle included still another version of~HOL,
    1.52 +  with explicit type inference rules~\cite{paulson-COLOG}.  This version no
    1.53 +  longer exists, but \thydx{ZF} supports a similar style of reasoning.}
    1.54 +follows $\lambda$-calculus and functional programming.  Function application
    1.55 +is curried.  To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to
    1.56 +the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$.  There is no
    1.57 +`apply' operator as in \thydx{ZF}.  Note that $f(a,b)$ means ``$f$ applied to
    1.58 +the pair $(a,b)$'' in HOL.  We write ordered pairs as $(a,b)$, not $\langle
    1.59 +a,b\rangle$ as in ZF.
    1.60 +
    1.61 +HOL has a distinct feel, compared with ZF and CTT.  It identifies object-level
    1.62 +types with meta-level types, taking advantage of Isabelle's built-in
    1.63 +type-checker.  It identifies object-level functions with meta-level functions,
    1.64 +so it uses Isabelle's operations for abstraction and application.
    1.65 +
    1.66 +These identifications allow Isabelle to support HOL particularly nicely, but
    1.67 +they also mean that HOL requires more sophistication from the user --- in
    1.68 +particular, an understanding of Isabelle's type system.  Beginners should work
    1.69 +with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.
    1.70  
    1.71  
    1.72  \begin{figure}
    1.73 @@ -123,7 +116,7 @@
    1.74           & | & "?!~~" id~id^* " . " formula \\
    1.75    \end{array}
    1.76  \]
    1.77 -\caption{Full grammar for \HOL} \label{hol-grammar}
    1.78 +\caption{Full grammar for HOL} \label{hol-grammar}
    1.79  \end{figure} 
    1.80  
    1.81  
    1.82 @@ -135,12 +128,11 @@
    1.83  $\lnot(a=b)$.
    1.84  
    1.85  \begin{warn}
    1.86 -  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
    1.87 -  using equality.  But equality has a high priority, as befitting a
    1.88 -  relation, while if-and-only-if typically has the lowest priority.  Thus,
    1.89 -  $\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.
    1.90 -  When using $=$ to mean logical equivalence, enclose both operands in
    1.91 -  parentheses.
    1.92 +  HOL has no if-and-only-if connective; logical equivalence is expressed using
    1.93 +  equality.  But equality has a high priority, as befitting a relation, while
    1.94 +  if-and-only-if typically has the lowest priority.  Thus, $\lnot\lnot P=P$
    1.95 +  abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.  When using $=$
    1.96 +  to mean logical equivalence, enclose both operands in parentheses.
    1.97  \end{warn}
    1.98  
    1.99  \subsection{Types and overloading}
   1.100 @@ -156,7 +148,7 @@
   1.101    term} if $\sigma$ and~$\tau$ do, allowing quantification over
   1.102  functions.
   1.103  
   1.104 -\HOL\ allows new types to be declared as subsets of existing types;
   1.105 +HOL allows new types to be declared as subsets of existing types;
   1.106  see~{\S}\ref{sec:HOL:Types}.  ML-like datatypes can also be declared; see
   1.107  ~{\S}\ref{sec:HOL:datatype}.
   1.108  
   1.109 @@ -218,12 +210,11 @@
   1.110  
   1.111  \subsection{Binders}
   1.112  
   1.113 -Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for
   1.114 -some~$x$ satisfying~$P$, if such exists.  Since all terms in \HOL\ 
   1.115 -denote something, a description is always meaningful, but we do not
   1.116 -know its value unless $P$ defines it uniquely.  We may write
   1.117 -descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
   1.118 -\hbox{\tt SOME~$x$.~$P[x]$}.
   1.119 +Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$
   1.120 +satisfying~$P$, if such exists.  Since all terms in HOL denote something, a
   1.121 +description is always meaningful, but we do not know its value unless $P$
   1.122 +defines it uniquely.  We may write descriptions as \cdx{Eps}($\lambda x.
   1.123 +P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.
   1.124  
   1.125  Existential quantification is defined by
   1.126  \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
   1.127 @@ -272,7 +263,7 @@
   1.128  the constant~\cdx{Let}.  It can be expanded by rewriting with its
   1.129  definition, \tdx{Let_def}.
   1.130  
   1.131 -\HOL\ also defines the basic syntax
   1.132 +HOL also defines the basic syntax
   1.133  \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
   1.134  as a uniform means of expressing \texttt{case} constructs.  Therefore \texttt{case}
   1.135  and \sdx{of} are reserved words.  Initially, this is mere syntax and has no
   1.136 @@ -305,9 +296,8 @@
   1.137  \caption{The \texttt{HOL} rules} \label{hol-rules}
   1.138  \end{figure}
   1.139  
   1.140 -Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
   1.141 -with their~{\ML} names.  Some of the rules deserve additional
   1.142 -comments:
   1.143 +Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
   1.144 +their~{\ML} names.  Some of the rules deserve additional comments:
   1.145  \begin{ttdescription}
   1.146  \item[\tdx{ext}] expresses extensionality of functions.
   1.147  \item[\tdx{iff}] asserts that logically equivalent formulae are
   1.148 @@ -342,14 +332,14 @@
   1.149  \end{figure}
   1.150  
   1.151  
   1.152 -\HOL{} follows standard practice in higher-order logic: only a few
   1.153 -connectives are taken as primitive, with the remainder defined obscurely
   1.154 +HOL follows standard practice in higher-order logic: only a few connectives
   1.155 +are taken as primitive, with the remainder defined obscurely
   1.156  (Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
   1.157  corresponding definitions \cite[page~270]{mgordon-hol} using
   1.158 -object-equality~({\tt=}), which is possible because equality in
   1.159 -higher-order logic may equate formulae and even functions over formulae.
   1.160 -But theory~\HOL{}, like all other Isabelle theories, uses
   1.161 -meta-equality~({\tt==}) for definitions.
   1.162 +object-equality~({\tt=}), which is possible because equality in higher-order
   1.163 +logic may equate formulae and even functions over formulae.  But theory~HOL,
   1.164 +like all other Isabelle theories, uses meta-equality~({\tt==}) for
   1.165 +definitions.
   1.166  \begin{warn}
   1.167  The definitions above should never be expanded and are shown for completeness
   1.168  only.  Instead users should reason in terms of the derived rules shown below
   1.169 @@ -401,7 +391,7 @@
   1.170  \subcaption{Logical equivalence}
   1.171  
   1.172  \end{ttbox}
   1.173 -\caption{Derived rules for \HOL} \label{hol-lemmas1}
   1.174 +\caption{Derived rules for HOL} \label{hol-lemmas1}
   1.175  \end{figure}
   1.176  
   1.177  
   1.178 @@ -584,8 +574,8 @@
   1.179  \section{A formulation of set theory}
   1.180  Historically, higher-order logic gives a foundation for Russell and
   1.181  Whitehead's theory of classes.  Let us use modern terminology and call them
   1.182 -{\bf sets}, but note that these sets are distinct from those of {\ZF} set
   1.183 -theory, and behave more like {\ZF} classes.
   1.184 +{\bf sets}, but note that these sets are distinct from those of ZF set theory,
   1.185 +and behave more like ZF classes.
   1.186  \begin{itemize}
   1.187  \item
   1.188  Sets are given by predicates over some type~$\sigma$.  Types serve to
   1.189 @@ -597,17 +587,17 @@
   1.190  Although sets may contain other sets as elements, the containing set must
   1.191  have a more complex type.
   1.192  \end{itemize}
   1.193 -Finite unions and intersections have the same behaviour in \HOL\ as they
   1.194 -do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
   1.195 -denoting the universal set for the given type.
   1.196 +Finite unions and intersections have the same behaviour in HOL as they do
   1.197 +in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
   1.198 +universal set for the given type.
   1.199  
   1.200  \subsection{Syntax of set theory}\index{*set type}
   1.201 -\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
   1.202 -essentially the same as $\alpha\To bool$.  The new type is defined for
   1.203 -clarity and to avoid complications involving function types in unification.
   1.204 -The isomorphisms between the two types are declared explicitly.  They are
   1.205 -very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
   1.206 -\hbox{\tt op :} maps in the other direction (ignoring argument order).
   1.207 +HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially
   1.208 +the same as $\alpha\To bool$.  The new type is defined for clarity and to
   1.209 +avoid complications involving function types in unification.  The isomorphisms
   1.210 +between the two types are declared explicitly.  They are very natural:
   1.211 +\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
   1.212 +maps in the other direction (ignoring argument order).
   1.213  
   1.214  Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
   1.215  translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
   1.216 @@ -623,11 +613,11 @@
   1.217    \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
   1.218  \end{eqnarray*}
   1.219  
   1.220 -The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
   1.221 -that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
   1.222 -occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
   1.223 -x. P[x])$.  It defines sets by absolute comprehension, which is impossible
   1.224 -in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
   1.225 +The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of
   1.226 +suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain
   1.227 +free occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.
   1.228 +P[x])$.  It defines sets by absolute comprehension, which is impossible in~ZF;
   1.229 +the type of~$x$ implicitly restricts the comprehension.
   1.230  
   1.231  The set theory defines two {\bf bounded quantifiers}:
   1.232  \begin{eqnarray*}
   1.233 @@ -867,14 +857,13 @@
   1.234  
   1.235  
   1.236  Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
   1.237 -obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
   1.238 -such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
   1.239 -are designed for classical reasoning; the rules \tdx{subsetD},
   1.240 -\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
   1.241 -strictly necessary but yield more natural proofs.  Similarly,
   1.242 -\tdx{equalityCE} supports classical reasoning about extensionality,
   1.243 -after the fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for
   1.244 -proofs pertaining to set theory.
   1.245 +obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such
   1.246 +as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
   1.247 +reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
   1.248 +not strictly necessary but yield more natural proofs.  Similarly,
   1.249 +\tdx{equalityCE} supports classical reasoning about extensionality, after the
   1.250 +fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for proofs
   1.251 +pertaining to set theory.
   1.252  
   1.253  Figure~\ref{hol-subset} presents lattice properties of the subset relation.
   1.254  Unions form least upper bounds; non-empty intersections form greatest lower
   1.255 @@ -927,7 +916,7 @@
   1.256  \section{Generic packages}
   1.257  \label{sec:HOL:generic-packages}
   1.258  
   1.259 -\HOL\ instantiates most of Isabelle's generic packages, making available the
   1.260 +HOL instantiates most of Isabelle's generic packages, making available the
   1.261  simplifier and the classical reasoner.
   1.262  
   1.263  \subsection{Simplification and substitution}
   1.264 @@ -972,17 +961,17 @@
   1.265  additional (first) subgoal.
   1.266  \end{ttdescription}
   1.267  
   1.268 - \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
   1.269 -  for an equality throughout a subgoal and its hypotheses.  This tactic uses
   1.270 -  \HOL's general substitution rule.
   1.271 +HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
   1.272 +equality throughout a subgoal and its hypotheses.  This tactic uses HOL's
   1.273 +general substitution rule.
   1.274  
   1.275  \subsubsection{Case splitting}
   1.276  \label{subsec:HOL:case:splitting}
   1.277  
   1.278 -\HOL{} also provides convenient means for case splitting during
   1.279 -rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
   1.280 -then\dots else\dots} often require a case distinction on $b$. This is
   1.281 -expressed by the theorem \tdx{split_if}:
   1.282 +HOL also provides convenient means for case splitting during rewriting. Goals
   1.283 +containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
   1.284 +often require a case distinction on $b$. This is expressed by the theorem
   1.285 +\tdx{split_if}:
   1.286  $$
   1.287  \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
   1.288  ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
   1.289 @@ -1035,9 +1024,9 @@
   1.290  
   1.291  \subsection{Classical reasoning}
   1.292  
   1.293 -\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
   1.294 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
   1.295 -rule; recall Fig.\ts\ref{hol-lemmas2} above.
   1.296 +HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
   1.297 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
   1.298 +Fig.\ts\ref{hol-lemmas2} above.
   1.299  
   1.300  The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and
   1.301  {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
   1.302 @@ -1143,11 +1132,10 @@
   1.303  
   1.304  
   1.305  \section{Types}\label{sec:HOL:Types}
   1.306 -This section describes \HOL's basic predefined types ($\alpha \times
   1.307 -\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
   1.308 -introducing new types in general.  The most important type
   1.309 -construction, the \texttt{datatype}, is treated separately in
   1.310 -{\S}\ref{sec:HOL:datatype}.
   1.311 +This section describes HOL's basic predefined types ($\alpha \times \beta$,
   1.312 +$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new
   1.313 +types in general.  The most important type construction, the
   1.314 +\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.
   1.315  
   1.316  
   1.317  \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
   1.318 @@ -1407,7 +1395,7 @@
   1.319  
   1.320  \subsection{Numerical types and numerical reasoning}
   1.321  
   1.322 -The integers (type \tdx{int}) are also available in \HOL, and the reals (type
   1.323 +The integers (type \tdx{int}) are also available in HOL, and the reals (type
   1.324  \tdx{real}) are available in the logic image \texttt{HOL-Real}.  They support
   1.325  the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
   1.326  multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the
   1.327 @@ -1608,14 +1596,14 @@
   1.328  
   1.329  \subsection{Introducing new types} \label{sec:typedef}
   1.330  
   1.331 -The \HOL-methodology dictates that all extensions to a theory should
   1.332 -be \textbf{definitional}.  The type definition mechanism that
   1.333 -meets this criterion is \ttindex{typedef}.  Note that \emph{type synonyms},
   1.334 -which are inherited from {\Pure} and described elsewhere, are just
   1.335 -syntactic abbreviations that have no logical meaning.
   1.336 +The HOL-methodology dictates that all extensions to a theory should be
   1.337 +\textbf{definitional}.  The type definition mechanism that meets this
   1.338 +criterion is \ttindex{typedef}.  Note that \emph{type synonyms}, which are
   1.339 +inherited from Pure and described elsewhere, are just syntactic abbreviations
   1.340 +that have no logical meaning.
   1.341  
   1.342  \begin{warn}
   1.343 -  Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
   1.344 +  Types in HOL must be non-empty; otherwise the quantifier rules would be
   1.345    unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
   1.346  \end{warn}
   1.347  A \bfindex{type definition} identifies the new type with a subset of
   1.348 @@ -1679,8 +1667,8 @@
   1.349  stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
   1.350  and its inverse $Abs_T$.
   1.351  \end{itemize}
   1.352 -Below are two simple examples of \HOL\ type definitions.  Non-emptiness
   1.353 -is proved automatically here.
   1.354 +Below are two simple examples of HOL type definitions.  Non-emptiness is
   1.355 +proved automatically here.
   1.356  \begin{ttbox}
   1.357  typedef unit = "{\ttlbrace}True{\ttrbrace}"
   1.358  
   1.359 @@ -1709,7 +1697,7 @@
   1.360  arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
   1.361  \end{ttbox}
   1.362  in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
   1.363 -class of all \HOL\ types.
   1.364 +class of all HOL types.
   1.365  \end{warn}
   1.366  
   1.367  
   1.368 @@ -2746,7 +2734,7 @@
   1.369  \item \textit{function} is the name of the function, either as an \textit{id}
   1.370    or a \textit{string}.  
   1.371    
   1.372 -\item \textit{rel} is a {\HOL} expression for the well-founded termination
   1.373 +\item \textit{rel} is a HOL expression for the well-founded termination
   1.374    relation.
   1.375    
   1.376  \item \textit{congruence rules} are required only in highly exceptional
   1.377 @@ -2852,14 +2840,14 @@
   1.378  proves some theorems.  Each definition creates an \ML\ structure, which is a
   1.379  substructure of the main theory structure.
   1.380  
   1.381 -This package is related to the \ZF\ one, described in a separate
   1.382 +This package is related to the ZF one, described in a separate
   1.383  paper,%
   1.384  \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
   1.385    distributed with Isabelle.}  %
   1.386  which you should refer to in case of difficulties.  The package is simpler
   1.387 -than \ZF's thanks to \HOL's extra-logical automatic type-checking.  The types
   1.388 -of the (co)inductive sets determine the domain of the fixedpoint definition,
   1.389 -and the package does not have to use inference rules for type-checking.
   1.390 +than ZF's thanks to HOL's extra-logical automatic type-checking.  The types of
   1.391 +the (co)inductive sets determine the domain of the fixedpoint definition, and
   1.392 +the package does not have to use inference rules for type-checking.
   1.393  
   1.394  
   1.395  \subsection{The result structure}
   1.396 @@ -2990,10 +2978,9 @@
   1.397  and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}.  The induction
   1.398  rule is \texttt{Fin.induct}.
   1.399  
   1.400 -For another example, here is a theory file defining the accessible
   1.401 -part of a relation.  The paper
   1.402 -\cite{paulson-CADE} discusses a \ZF\ version of this example in more
   1.403 -detail.
   1.404 +For another example, here is a theory file defining the accessible part of a
   1.405 +relation.  The paper \cite{paulson-CADE} discusses a ZF version of this
   1.406 +example in more detail.
   1.407  \begin{ttbox}
   1.408  Acc = WF + Inductive +
   1.409  
   1.410 @@ -3041,9 +3028,9 @@
   1.411  $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
   1.412  and $\eta$ reduction~\cite{Nipkow-CR}.
   1.413  
   1.414 -Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of
   1.415 -substitutions and unifiers.  It is based on Paulson's previous
   1.416 -mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
   1.417 +Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory
   1.418 +of substitutions and unifiers.  It is based on Paulson's previous
   1.419 +mechanisation in LCF~\cite{paulson85} of Manna and Waldinger's
   1.420  theory~\cite{mw81}.  It demonstrates a complicated use of \texttt{recdef},
   1.421  with nested recursion.
   1.422  
   1.423 @@ -3053,8 +3040,8 @@
   1.424  \item Theory \texttt{PropLog} proves the soundness and completeness of
   1.425    classical propositional logic, given a truth table semantics.  The only
   1.426    connective is $\imp$.  A Hilbert-style axiom system is specified, and its
   1.427 -  set of theorems defined inductively.  A similar proof in \ZF{} is
   1.428 -  described elsewhere~\cite{paulson-set-II}.
   1.429 +  set of theorems defined inductively.  A similar proof in ZF is described
   1.430 +  elsewhere~\cite{paulson-set-II}.
   1.431  
   1.432  \item Theory \texttt{Term} defines the datatype \texttt{term}.
   1.433  
   1.434 @@ -3083,7 +3070,7 @@
   1.435  \end{itemize}
   1.436  
   1.437  Directory \texttt{HOL/ex} contains other examples and experimental proofs in
   1.438 -{\HOL}.  
   1.439 +HOL.
   1.440  \begin{itemize}
   1.441  \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}
   1.442    to define recursive functions.  Another example is \texttt{Fib}, which
   1.443 @@ -3135,7 +3122,7 @@
   1.444  of~$\alpha$.  This version states that for every function from $\alpha$ to
   1.445  its powerset, some subset is outside its range.  
   1.446  
   1.447 -The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
   1.448 +The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and
   1.449  the operator \cdx{range}.
   1.450  \begin{ttbox}
   1.451  context Set.thy;
   1.452 @@ -3205,12 +3192,11 @@
   1.453  {\out No subgoals!}
   1.454  \end{ttbox}
   1.455  How much creativity is required?  As it happens, Isabelle can prove this
   1.456 -theorem automatically.  The default classical set \texttt{claset()} contains rules
   1.457 -for most of the constructs of \HOL's set theory.  We must augment it with
   1.458 -\tdx{equalityCE} to break up set equalities, and then apply best-first
   1.459 -search.  Depth-first search would diverge, but best-first search
   1.460 -successfully navigates through the large search space.
   1.461 -\index{search!best-first}
   1.462 +theorem automatically.  The default classical set \texttt{claset()} contains
   1.463 +rules for most of the constructs of HOL's set theory.  We must augment it with
   1.464 +\tdx{equalityCE} to break up set equalities, and then apply best-first search.
   1.465 +Depth-first search would diverge, but best-first search successfully navigates
   1.466 +through the large search space.  \index{search!best-first}
   1.467  \begin{ttbox}
   1.468  choplev 0;
   1.469  {\out Level 0}
     2.1 --- a/doc-src/HOL/Makefile	Mon Aug 28 13:50:24 2000 +0200
     2.2 +++ b/doc-src/HOL/Makefile	Mon Aug 28 13:52:38 2000 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  NAME = logics-HOL
     2.6  FILES = logics-HOL.tex ../Logics/syntax.tex HOL.tex \
     2.7 -	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
     2.8 +	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
     2.9  
    2.10  dvi: $(NAME).dvi
    2.11  
     3.1 --- a/doc-src/HOL/logics-HOL.tex	Mon Aug 28 13:50:24 2000 +0200
     3.2 +++ b/doc-src/HOL/logics-HOL.tex	Mon Aug 28 13:52:38 2000 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  %% $Id$
     3.5  \documentclass[12pt,a4paper]{report}
     3.6 -\usepackage{graphicx,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
     3.7 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
     3.8  
     3.9  %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    3.10  %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
     4.1 --- a/doc-src/Inductive/Makefile	Mon Aug 28 13:50:24 2000 +0200
     4.2 +++ b/doc-src/Inductive/Makefile	Mon Aug 28 13:52:38 2000 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  include ../Makefile.in
     4.5  
     4.6  NAME = ind-defs
     4.7 -FILES = ind-defs.tex ../proof.sty ../iman.sty ../extra.sty ../manual.bib
     4.8 +FILES = ind-defs.tex ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
     4.9  
    4.10  dvi: $(NAME).dvi
    4.11  
     5.1 --- a/doc-src/Inductive/ind-defs.tex	Mon Aug 28 13:50:24 2000 +0200
     5.2 +++ b/doc-src/Inductive/ind-defs.tex	Mon Aug 28 13:52:38 2000 +0200
     5.3 @@ -1,6 +1,6 @@
     5.4  %% $Id$
     5.5  \documentclass[12pt,a4paper]{article}
     5.6 -\usepackage{latexsym,../iman,../extra,../proof,../pdfsetup}
     5.7 +\usepackage{latexsym,../iman,../extra,../ttbox,../proof,../pdfsetup}
     5.8  
     5.9  \newif\ifshort%''Short'' means a published version, not the documentation
    5.10  \shortfalse%%%%%\shorttrue
     6.1 --- a/doc-src/Intro/Makefile	Mon Aug 28 13:50:24 2000 +0200
     6.2 +++ b/doc-src/Intro/Makefile	Mon Aug 28 13:52:38 2000 +0200
     6.3 @@ -13,7 +13,7 @@
     6.4  
     6.5  NAME = intro
     6.6  FILES = intro.tex foundations.tex getting.tex advanced.tex \
     6.7 -	../proof.sty ../iman.sty ../extra.sty ../manual.bib
     6.8 +	../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
     6.9  
    6.10  dvi: $(NAME).dvi
    6.11  
     7.1 --- a/doc-src/Intro/advanced.tex	Mon Aug 28 13:50:24 2000 +0200
     7.2 +++ b/doc-src/Intro/advanced.tex	Mon Aug 28 13:52:38 2000 +0200
     7.3 @@ -293,7 +293,7 @@
     7.4  \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
     7.5      Manual}}{App.\ts\ref{app:TheorySyntax}}.  Also note that
     7.6  object-logics may add further theory sections, for example
     7.7 -\texttt{typedef}, \texttt{datatype} in \HOL.
     7.8 +\texttt{typedef}, \texttt{datatype} in HOL.
     7.9  
    7.10  All the declaration parts can be omitted or repeated and may appear in
    7.11  any order, except that the {\ML} section must be last (after the {\tt
    7.12 @@ -302,7 +302,7 @@
    7.13  theories, inheriting their types, constants, syntax, etc.  The theory
    7.14  \thydx{Pure} contains nothing but Isabelle's meta-logic.  The variant
    7.15  \thydx{CPure} offers the more usual higher-order function application
    7.16 -syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure.
    7.17 +syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.
    7.18  
    7.19  Each theory definition must reside in a separate file, whose name is
    7.20  the theory's with {\tt.thy} appended.  Calling
    7.21 @@ -964,12 +964,11 @@
    7.22  
    7.23  \index{simplification}\index{examples!of simplification} 
    7.24  
    7.25 -Isabelle's simplification tactics repeatedly apply equations to a
    7.26 -subgoal, perhaps proving it.  For efficiency, the rewrite rules must
    7.27 -be packaged into a {\bf simplification set},\index{simplification
    7.28 -  sets} or {\bf simpset}.  We augment the implicit simpset of {\FOL}
    7.29 -with the equations proved in the previous section, namely $0+n=n$ and
    7.30 -$\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
    7.31 +Isabelle's simplification tactics repeatedly apply equations to a subgoal,
    7.32 +perhaps proving it.  For efficiency, the rewrite rules must be packaged into a
    7.33 +{\bf simplification set},\index{simplification sets} or {\bf simpset}.  We
    7.34 +augment the implicit simpset of FOL with the equations proved in the previous
    7.35 +section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
    7.36  \begin{ttbox}
    7.37  Addsimps [add_0, add_Suc];
    7.38  \end{ttbox}
     8.1 --- a/doc-src/Intro/foundations.tex	Mon Aug 28 13:50:24 2000 +0200
     8.2 +++ b/doc-src/Intro/foundations.tex	Mon Aug 28 13:52:38 2000 +0200
     8.3 @@ -441,20 +441,18 @@
     8.4  Under similar conditions, a signature can be extended.  Signatures are
     8.5  managed internally by Isabelle; users seldom encounter them.
     8.6  
     8.7 -\index{theories|bold} A {\bf theory} consists of a signature plus a
     8.8 -collection of axioms.  The {\Pure} theory contains only the
     8.9 -meta-logic.  Theories can be combined provided their signatures are
    8.10 -compatible.  A theory definition extends an existing theory with
    8.11 -further signature specifications --- classes, types, constants and
    8.12 -mixfix declarations --- plus lists of axioms and definitions etc.,
    8.13 -expressed as strings to be parsed.  A theory can formalize a small
    8.14 -piece of mathematics, such as lists and their operations, or an entire
    8.15 -logic.  A mathematical development typically involves many theories in
    8.16 -a hierarchy.  For example, the {\Pure} theory could be extended to
    8.17 -form a theory for Fig.\ts\ref{fol-fig}; this could be extended in two
    8.18 -separate ways to form a theory for natural numbers and a theory for
    8.19 -lists; the union of these two could be extended into a theory defining
    8.20 -the length of a list:
    8.21 +\index{theories|bold} A {\bf theory} consists of a signature plus a collection
    8.22 +of axioms.  The Pure theory contains only the meta-logic.  Theories can be
    8.23 +combined provided their signatures are compatible.  A theory definition
    8.24 +extends an existing theory with further signature specifications --- classes,
    8.25 +types, constants and mixfix declarations --- plus lists of axioms and
    8.26 +definitions etc., expressed as strings to be parsed.  A theory can formalize a
    8.27 +small piece of mathematics, such as lists and their operations, or an entire
    8.28 +logic.  A mathematical development typically involves many theories in a
    8.29 +hierarchy.  For example, the Pure theory could be extended to form a theory
    8.30 +for Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form
    8.31 +a theory for natural numbers and a theory for lists; the union of these two
    8.32 +could be extended into a theory defining the length of a list:
    8.33  \begin{tt}
    8.34  \[
    8.35  \begin{array}{c@{}c@{}c@{}c@{}c}
     9.1 --- a/doc-src/Intro/getting.tex	Mon Aug 28 13:50:24 2000 +0200
     9.2 +++ b/doc-src/Intro/getting.tex	Mon Aug 28 13:52:38 2000 +0200
     9.3 @@ -26,7 +26,7 @@
     9.4  isabelle FOL
     9.5  \end{ttbox}
     9.6  Note that just typing \texttt{isabelle} usually brings up higher-order logic
     9.7 -(\HOL) by default.
     9.8 +(HOL) by default.
     9.9  
    9.10  
    9.11  \subsection{Lexical matters}
    9.12 @@ -110,8 +110,8 @@
    9.13    t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
    9.14  \end{array}  
    9.15  \]
    9.16 -Note that \HOL{} uses its traditional ``higher-order'' syntax for application,
    9.17 -which differs from that used in \FOL\@.
    9.18 +Note that HOL uses its traditional ``higher-order'' syntax for application,
    9.19 +which differs from that used in FOL.
    9.20  
    9.21  The theorems and rules of an object-logic are represented by theorems in
    9.22  the meta-logic, which are expressed using meta-formulae.  Since the
    9.23 @@ -228,10 +228,10 @@
    9.24    to have subscript zero, improving readability and reducing subscript
    9.25    growth.
    9.26  \end{ttdescription}
    9.27 -The rules of a theory are normally bound to \ML\ identifiers.  Suppose we
    9.28 -are running an Isabelle session containing theory~\FOL, natural deduction
    9.29 -first-order logic.\footnote{For a listing of the \FOL{} rules and their
    9.30 -  \ML{} names, turn to
    9.31 +The rules of a theory are normally bound to \ML\ identifiers.  Suppose we are
    9.32 +running an Isabelle session containing theory~FOL, natural deduction
    9.33 +first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
    9.34 +  names, turn to
    9.35  \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
    9.36             {page~\pageref{fol-rules}}.}
    9.37  Let us try an example given in~\S\ref{joining}.  We
    10.1 --- a/doc-src/Intro/intro.tex	Mon Aug 28 13:50:24 2000 +0200
    10.2 +++ b/doc-src/Intro/intro.tex	Mon Aug 28 13:52:38 2000 +0200
    10.3 @@ -1,5 +1,5 @@
    10.4  \documentclass[12pt,a4paper]{article}
    10.5 -\usepackage{graphicx,../iman,../extra,../proof,../pdfsetup}
    10.6 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup}
    10.7  
    10.8  %% $Id$
    10.9  %% run    bibtex intro         to prepare bibliography
    11.1 --- a/doc-src/IsarRef/Makefile	Mon Aug 28 13:50:24 2000 +0200
    11.2 +++ b/doc-src/IsarRef/Makefile	Mon Aug 28 13:52:38 2000 +0200
    11.3 @@ -15,7 +15,8 @@
    11.4  
    11.5  FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
    11.6  	generic.tex hol.tex refcard.tex conversion.tex ../isar.sty \
    11.7 -	../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
    11.8 +	../rail.sty ../railsetup.sty ../proof.sty ../iman.sty \
    11.9 +	../extra.sty ../ttbox.sty ../manual.bib
   11.10  
   11.11  dvi: $(NAME).dvi
   11.12  
    12.1 --- a/doc-src/IsarRef/hol.tex	Mon Aug 28 13:50:24 2000 +0200
    12.2 +++ b/doc-src/IsarRef/hol.tex	Mon Aug 28 13:52:38 2000 +0200
    12.3 @@ -231,11 +231,11 @@
    12.4    The rule is determined as follows, according to the facts and arguments
    12.5    passed to the $cases$ method:
    12.6    \begin{matharray}{llll}
    12.7 -    \text{facts}    &       & \text{arguments} & \text{rule} \\\hline
    12.8 -                    & cases &           & \text{classical case split} \\
    12.9 -                    & cases & t         & \text{datatype exhaustion (type of $t$)} \\
   12.10 -    \edrv a \in A   & cases & \dots     & \text{inductive set elimination (of $A$)} \\
   12.11 -    \dots           & cases & \dots ~ R & \text{explicit rule $R$} \\
   12.12 +    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
   12.13 +                    & cases &           & \Text{classical case split} \\
   12.14 +                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
   12.15 +    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
   12.16 +    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
   12.17    \end{matharray}
   12.18    
   12.19    Several instantiations may be given, referring to the \emph{suffix} of
   12.20 @@ -257,10 +257,10 @@
   12.21  \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
   12.22    induction rules, which are determined as follows:
   12.23    \begin{matharray}{llll}
   12.24 -    \text{facts}    &        & \text{arguments} & \text{rule} \\\hline
   12.25 -                    & induct & P ~ x ~ \dots & \text{datatype induction (type of $x$)} \\
   12.26 -    \edrv x \in A   & induct & \dots         & \text{set induction (of $A$)} \\
   12.27 -    \dots           & induct & \dots ~ R     & \text{explicit rule $R$} \\
   12.28 +    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
   12.29 +                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
   12.30 +    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
   12.31 +    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
   12.32    \end{matharray}
   12.33    
   12.34    Several instantiations may be given, each referring to some part of a mutual
    13.1 --- a/doc-src/IsarRef/isar-ref.tex	Mon Aug 28 13:50:24 2000 +0200
    13.2 +++ b/doc-src/IsarRef/isar-ref.tex	Mon Aug 28 13:52:38 2000 +0200
    13.3 @@ -9,7 +9,7 @@
    13.4  
    13.5  
    13.6  \documentclass[12pt,a4paper,fleqn]{report}
    13.7 -\usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
    13.8 +\usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}
    13.9  
   13.10  \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
   13.11  \author{\emph{Markus Wenzel} \\ TU M\"unchen}
    14.1 --- a/doc-src/IsarRef/pure.tex	Mon Aug 28 13:50:24 2000 +0200
    14.2 +++ b/doc-src/IsarRef/pure.tex	Mon Aug 28 13:52:38 2000 +0200
    14.3 @@ -687,7 +687,7 @@
    14.4  Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect
    14.5  multiple facts to be given in their proper order, corresponding to a prefix of
    14.6  the premises of the rule involved.  Note that positions may be easily skipped
    14.7 -using something like $\FROM{\text{\texttt{_}}~a~b}$, for example.  This
    14.8 +using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example.  This
    14.9  involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be
   14.10  bound in Isabelle/Pure as ``\texttt{_}''
   14.11  (underscore).\indexisarthm{_@\texttt{_}}
    15.1 --- a/doc-src/IsarRef/refcard.tex	Mon Aug 28 13:50:24 2000 +0200
    15.2 +++ b/doc-src/IsarRef/refcard.tex	Mon Aug 28 13:52:38 2000 +0200
    15.3 @@ -15,7 +15,7 @@
    15.4    $\BG~\dots~\EN$ & declare explicit blocks \\
    15.5    $\NEXT$ & switch implicit blocks \\
    15.6    $\NOTE{a}{\vec b}$ & reconsider facts \\
    15.7 -  $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
    15.8 +  $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\
    15.9  \end{tabular}
   15.10  
   15.11  \begin{matharray}{rcl}
   15.12 @@ -61,13 +61,13 @@
   15.13    \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
   15.14    \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
   15.15    \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
   15.16 -%  & & \text{(permissive assumption)} \\
   15.17 +%  & & \Text{(permissive assumption)} \\
   15.18    \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
   15.19 -%  & & \text{(definitional assumption)} \\
   15.20 +%  & & \Text{(definitional assumption)} \\
   15.21    \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
   15.22 -%  & & \text{(generalized existence)} \\
   15.23 +%  & & \Text{(generalized existence)} \\
   15.24    \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
   15.25 -%  & & \text{(named context)} \\[0.5ex]
   15.26 +%  & & \Text{(named context)} \\[0.5ex]
   15.27    \SORRY & \approx & \BY{cheating} \\
   15.28  \end{matharray}
   15.29  
   15.30 @@ -75,11 +75,11 @@
   15.31  \subsection{Diagnostic commands}
   15.32  
   15.33  \begin{matharray}{ll}
   15.34 -  \isarkeyword{pr} & \text{print current state} \\
   15.35 -  \isarkeyword{thm}~\vec a & \text{print theorems} \\
   15.36 -  \isarkeyword{term}~t & \text{print term} \\
   15.37 -  \isarkeyword{prop}~\phi & \text{print meta-level proposition} \\
   15.38 -  \isarkeyword{typ}~\tau & \text{print meta-level type} \\
   15.39 +  \isarkeyword{pr} & \Text{print current state} \\
   15.40 +  \isarkeyword{thm}~\vec a & \Text{print theorems} \\
   15.41 +  \isarkeyword{term}~t & \Text{print term} \\
   15.42 +  \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\
   15.43 +  \isarkeyword{typ}~\tau & \Text{print meta-level type} \\
   15.44  \end{matharray}
   15.45  
   15.46  
   15.47 @@ -96,11 +96,11 @@
   15.48    $induct~\vec x$ & proof by induction (provides cases) \\[2ex]
   15.49  
   15.50    \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
   15.51 -  $-$ & \text{no rules} \\
   15.52 -  $intro~\vec a$ & \text{introduction rules} \\
   15.53 -  $intro_classes$ & \text{class introduction rules} \\
   15.54 -  $elim~\vec a$ & \text{elimination rules} \\
   15.55 -  $unfold~\vec a$ & \text{definitions} \\[2ex]
   15.56 +  $-$ & \Text{no rules} \\
   15.57 +  $intro~\vec a$ & \Text{introduction rules} \\
   15.58 +  $intro_classes$ & \Text{class introduction rules} \\
   15.59 +  $elim~\vec a$ & \Text{elimination rules} \\
   15.60 +  $unfold~\vec a$ & \Text{definitions} \\[2ex]
   15.61  
   15.62    \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
   15.63    $simp$, $simp_all$ & Simplifier (+ Splitter) \\
    16.1 --- a/doc-src/Logics/CTT.tex	Mon Aug 28 13:50:24 2000 +0200
    16.2 +++ b/doc-src/Logics/CTT.tex	Mon Aug 28 13:52:38 2000 +0200
    16.3 @@ -40,16 +40,16 @@
    16.4  Assumptions can use all the judgement forms, for instance to express that
    16.5  $B$ is a family of types over~$A$:
    16.6  \[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
    16.7 -To justify the {\CTT} formulation it is probably best to appeal directly
    16.8 -to the semantic explanations of the rules~\cite{martinlof84}, rather than
    16.9 -to the rules themselves.  The order of assumptions no longer matters,
   16.10 -unlike in standard Type Theory.  Contexts, which are typical of many modern
   16.11 -type theories, are difficult to represent in Isabelle.  In particular, it
   16.12 -is difficult to enforce that all the variables in a context are distinct.
   16.13 -\index{assumptions!in {\CTT}}
   16.14 +To justify the CTT formulation it is probably best to appeal directly to the
   16.15 +semantic explanations of the rules~\cite{martinlof84}, rather than to the
   16.16 +rules themselves.  The order of assumptions no longer matters, unlike in
   16.17 +standard Type Theory.  Contexts, which are typical of many modern type
   16.18 +theories, are difficult to represent in Isabelle.  In particular, it is
   16.19 +difficult to enforce that all the variables in a context are distinct.
   16.20 +\index{assumptions!in CTT}
   16.21  
   16.22 -The theory does not use polymorphism.  Terms in {\CTT} have type~\tydx{i}, the
   16.23 -type of individuals.  Types in {\CTT} have type~\tydx{t}.
   16.24 +The theory does not use polymorphism.  Terms in CTT have type~\tydx{i}, the
   16.25 +type of individuals.  Types in CTT have type~\tydx{t}.
   16.26  
   16.27  \begin{figure} \tabcolsep=1em  %wider spacing in tables
   16.28  \begin{center}
   16.29 @@ -81,29 +81,29 @@
   16.30    \cdx{tt}      & $i$                   & constructor
   16.31  \end{tabular}
   16.32  \end{center}
   16.33 -\caption{The constants of {\CTT}} \label{ctt-constants}
   16.34 +\caption{The constants of CTT} \label{ctt-constants}
   16.35  \end{figure}
   16.36  
   16.37  
   16.38 -{\CTT} supports all of Type Theory apart from list types, well-ordering
   16.39 -types, and universes.  Universes could be introduced {\em\`a la Tarski},
   16.40 -adding new constants as names for types.  The formulation {\em\`a la
   16.41 -  Russell}, where types denote themselves, is only possible if we identify
   16.42 -the meta-types~{\tt i} and~{\tt t}.  Most published formulations of
   16.43 -well-ordering types have difficulties involving extensionality of
   16.44 -functions; I suggest that you use some other method for defining recursive
   16.45 -types.  List types are easy to introduce by declaring new rules.
   16.46 +CTT supports all of Type Theory apart from list types, well-ordering types,
   16.47 +and universes.  Universes could be introduced {\em\`a la Tarski}, adding new
   16.48 +constants as names for types.  The formulation {\em\`a la Russell}, where
   16.49 +types denote themselves, is only possible if we identify the meta-types~{\tt
   16.50 +  i} and~{\tt t}.  Most published formulations of well-ordering types have
   16.51 +difficulties involving extensionality of functions; I suggest that you use
   16.52 +some other method for defining recursive types.  List types are easy to
   16.53 +introduce by declaring new rules.
   16.54  
   16.55 -{\CTT} uses the 1982 version of Type Theory, with extensional equality.
   16.56 -The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are
   16.57 -interchangeable.  Its rewriting tactics prove theorems of the form $a=b\in
   16.58 -A$.  It could be modified to have intensional equality, but rewriting
   16.59 -tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the
   16.60 -computation rules might require a separate simplifier.
   16.61 +CTT uses the 1982 version of Type Theory, with extensional equality.  The
   16.62 +computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
   16.63 +Its rewriting tactics prove theorems of the form $a=b\in A$.  It could be
   16.64 +modified to have intensional equality, but rewriting tactics would have to
   16.65 +prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
   16.66 +require a separate simplifier.
   16.67  
   16.68  
   16.69  \begin{figure} \tabcolsep=1em  %wider spacing in tables
   16.70 -\index{lambda abs@$\lambda$-abstractions!in \CTT}
   16.71 +\index{lambda abs@$\lambda$-abstractions!in CTT}
   16.72  \begin{center}
   16.73  \begin{tabular}{llrrr} 
   16.74    \it symbol &\it name     &\it meta-type & \it priority & \it description \\
   16.75 @@ -113,7 +113,7 @@
   16.76  \subcaption{Binders} 
   16.77  
   16.78  \begin{center}
   16.79 -\index{*"` symbol}\index{function applications!in \CTT}
   16.80 +\index{*"` symbol}\index{function applications!in CTT}
   16.81  \index{*"+ symbol}
   16.82  \begin{tabular}{rrrr} 
   16.83    \it symbol & \it meta-type    & \it priority & \it description \\ 
   16.84 @@ -160,7 +160,7 @@
   16.85  \]
   16.86  \end{center}
   16.87  \subcaption{Grammar}
   16.88 -\caption{Syntax of {\CTT}} \label{ctt-syntax}
   16.89 +\caption{Syntax of CTT} \label{ctt-syntax}
   16.90  \end{figure}
   16.91  
   16.92  %%%%\section{Generic Packages}  typedsimp.ML????????????????
   16.93 @@ -168,16 +168,16 @@
   16.94  
   16.95  \section{Syntax}
   16.96  The constants are shown in Fig.\ts\ref{ctt-constants}.  The infixes include
   16.97 -the function application operator (sometimes called `apply'), and the
   16.98 -2-place type operators.  Note that meta-level abstraction and application,
   16.99 -$\lambda x.b$ and $f(a)$, differ from object-level abstraction and
  16.100 -application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$.  A {\CTT}
  16.101 -function~$f$ is simply an individual as far as Isabelle is concerned: its
  16.102 -Isabelle type is~$i$, not say $i\To i$.
  16.103 +the function application operator (sometimes called `apply'), and the 2-place
  16.104 +type operators.  Note that meta-level abstraction and application, $\lambda
  16.105 +x.b$ and $f(a)$, differ from object-level abstraction and application,
  16.106 +\hbox{\tt lam $x$. $b$} and $b{\tt`}a$.  A CTT function~$f$ is simply an
  16.107 +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
  16.108 +$i\To i$.
  16.109  
  16.110 -The notation for~{\CTT} (Fig.\ts\ref{ctt-syntax}) is based on that of
  16.111 -Nordstr\"om et al.~\cite{nordstrom90}.  The empty type is called $F$ and
  16.112 -the one-element type is $T$; other finite types are built as $T+T+T$, etc.
  16.113 +The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
  16.114 +et al.~\cite{nordstrom90}.  The empty type is called $F$ and the one-element
  16.115 +type is $T$; other finite types are built as $T+T+T$, etc.
  16.116  
  16.117  \index{*SUM symbol}\index{*PROD symbol}
  16.118  Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
  16.119 @@ -387,7 +387,7 @@
  16.120            |] ==> snd(p) : B(fst(p))
  16.121  \end{ttbox}
  16.122  
  16.123 -\caption{Derived rules for {\CTT}} \label{ctt-derived}
  16.124 +\caption{Derived rules for CTT} \label{ctt-derived}
  16.125  \end{figure}
  16.126  
  16.127  
  16.128 @@ -470,7 +470,7 @@
  16.129  \section{Rule lists}
  16.130  The Type Theory tactics provide rewriting, type inference, and logical
  16.131  reasoning.  Many proof procedures work by repeatedly resolving certain Type
  16.132 -Theory rules against a proof state.  {\CTT} defines lists --- each with
  16.133 +Theory rules against a proof state.  CTT defines lists --- each with
  16.134  type
  16.135  \hbox{\tt thm list} --- of related rules. 
  16.136  \begin{ttdescription}
  16.137 @@ -514,14 +514,14 @@
  16.138  equal_tac       : thm list -> tactic
  16.139  intr_tac        : thm list -> tactic
  16.140  \end{ttbox}
  16.141 -Blind application of {\CTT} rules seldom leads to a proof.  The elimination
  16.142 +Blind application of CTT rules seldom leads to a proof.  The elimination
  16.143  rules, especially, create subgoals containing new unknowns.  These subgoals
  16.144  unify with anything, creating a huge search space.  The standard tactic
  16.145 -\ttindex{filt_resolve_tac} 
  16.146 +\ttindex{filt_resolve_tac}
  16.147  (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
  16.148          {\S\ref{filt_resolve_tac}})
  16.149  %
  16.150 -fails for goals that are too flexible; so does the {\CTT} tactic {\tt
  16.151 +fails for goals that are too flexible; so does the CTT tactic {\tt
  16.152    test_assume_tac}.  Used with the tactical \ttindex{REPEAT_FIRST} they
  16.153  achieve a simple kind of subgoal reordering: the less flexible subgoals are
  16.154  attempted first.  Do some single step proofs, or study the examples below,
  16.155 @@ -563,8 +563,8 @@
  16.156    CTT} equality rules and the built-in rewriting functor
  16.157  {\tt TSimpFun}.%
  16.158  \footnote{This should not be confused with Isabelle's main simplifier; {\tt
  16.159 -    TSimpFun} is only useful for {\CTT} and similar logics with type
  16.160 -  inference rules.  At present it is undocumented.} 
  16.161 +    TSimpFun} is only useful for CTT and similar logics with type inference
  16.162 +  rules.  At present it is undocumented.}
  16.163  %
  16.164  The rewrites include the computation rules and other equations.  The long
  16.165  versions of the other rules permit rewriting of subterms and subtypes.
  16.166 @@ -583,11 +583,11 @@
  16.167  
  16.168  
  16.169  \section{Tactics for logical reasoning}
  16.170 -Interpreting propositions as types lets {\CTT} express statements of
  16.171 -intuitionistic logic.  However, Constructive Type Theory is not just
  16.172 -another syntax for first-order logic.  There are fundamental differences.
  16.173 +Interpreting propositions as types lets CTT express statements of
  16.174 +intuitionistic logic.  However, Constructive Type Theory is not just another
  16.175 +syntax for first-order logic.  There are fundamental differences.
  16.176  
  16.177 -\index{assumptions!in {\CTT}}
  16.178 +\index{assumptions!in CTT}
  16.179  Can assumptions be deleted after use?  Not every occurrence of a type
  16.180  represents a proposition, and Type Theory assumptions declare variables.
  16.181  In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
  16.182 @@ -598,7 +598,7 @@
  16.183  refer to $z$ may render the subgoal unprovable: arguably,
  16.184  meaningless.
  16.185  
  16.186 -Isabelle provides several tactics for predicate calculus reasoning in \CTT:
  16.187 +Isabelle provides several tactics for predicate calculus reasoning in CTT:
  16.188  \begin{ttbox}
  16.189  mp_tac       : int -> tactic
  16.190  add_mp_tac   : int -> tactic
  16.191 @@ -728,7 +728,7 @@
  16.192  
  16.193  
  16.194  \section{The examples directory}
  16.195 -This directory contains examples and experimental proofs in {\CTT}.
  16.196 +This directory contains examples and experimental proofs in CTT.
  16.197  \begin{ttdescription}
  16.198  \item[CTT/ex/typechk.ML]
  16.199  contains simple examples of type-checking and type deduction.
    17.1 --- a/doc-src/Logics/LK.tex	Mon Aug 28 13:50:24 2000 +0200
    17.2 +++ b/doc-src/Logics/LK.tex	Mon Aug 28 13:52:38 2000 +0200
    17.3 @@ -18,8 +18,8 @@
    17.4  are polymorphic (many-sorted).  The type of formulae is~\tydx{o}, which
    17.5  belongs to class {\tt logic}.
    17.6  
    17.7 -\LK{} implements a classical logic theorem prover that is nearly as powerful
    17.8 -as the generic classical reasoner.  The simplifier is now available too.
    17.9 +LK implements a classical logic theorem prover that is nearly as powerful as
   17.10 +the generic classical reasoner.  The simplifier is now available too.
   17.11  
   17.12  To work in LK, start up Isabelle specifying  \texttt{Sequents} as the
   17.13  object-logic.  Once in Isabelle, change the context to theory \texttt{LK.thy}:
   17.14 @@ -179,17 +179,17 @@
   17.15  of formulae.
   17.16  
   17.17  The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$
   17.18 -satisfying~$P[a]$, if one exists and is unique.  Since all terms in \LK{}
   17.19 -denote something, a description is always meaningful, but we do not know
   17.20 -its value unless $P[x]$ defines it uniquely.  The Isabelle notation is
   17.21 -\hbox{\tt THE $x$.\ $P[x]$}.  The corresponding rule (Fig.\ts\ref{lk-rules})
   17.22 -does not entail the Axiom of Choice because it requires uniqueness.
   17.23 +satisfying~$P[a]$, if one exists and is unique.  Since all terms in LK denote
   17.24 +something, a description is always meaningful, but we do not know its value
   17.25 +unless $P[x]$ defines it uniquely.  The Isabelle notation is \hbox{\tt THE
   17.26 +  $x$.\ $P[x]$}.  The corresponding rule (Fig.\ts\ref{lk-rules}) does not
   17.27 +entail the Axiom of Choice because it requires uniqueness.
   17.28  
   17.29  Conditional expressions are available with the notation 
   17.30  \[ \dquotes
   17.31     "if"~formula~"then"~term~"else"~term. \]
   17.32  
   17.33 -Figure~\ref{lk-grammar} presents the grammar of \LK.  Traditionally,
   17.34 +Figure~\ref{lk-grammar} presents the grammar of LK.  Traditionally,
   17.35  \(\Gamma\) and \(\Delta\) are meta-variables for sequences.  In Isabelle's
   17.36  notation, the prefix~\verb|$| on a term makes it range over sequences.
   17.37  In a sequent, anything not prefixed by \verb|$| is taken as a formula.
   17.38 @@ -272,13 +272,13 @@
   17.39  
   17.40  \section{Automatic Proof}
   17.41  
   17.42 -\LK{} instantiates Isabelle's simplifier.  Both equality ($=$) and the
   17.43 +LK instantiates Isabelle's simplifier.  Both equality ($=$) and the
   17.44  biconditional ($\bimp$) may be used for rewriting.  The tactic
   17.45  \texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}).  With
   17.46  sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not
   17.47 -required; all the formulae{} in the sequent will be simplified.  The
   17.48 -left-hand formulae{} are taken as rewrite rules.  (Thus, the behaviour is what
   17.49 -you would normally expect from calling \texttt{Asm_full_simp_tac}.)
   17.50 +required; all the formulae{} in the sequent will be simplified.  The left-hand
   17.51 +formulae{} are taken as rewrite rules.  (Thus, the behaviour is what you would
   17.52 +normally expect from calling \texttt{Asm_full_simp_tac}.)
   17.53  
   17.54  For classical reasoning, several tactics are available:
   17.55  \begin{ttbox} 
   17.56 @@ -325,15 +325,13 @@
   17.57  These tactics refine a subgoal into two by applying the cut rule.  The cut
   17.58  formula is given as a string, and replaces some other formula in the sequent.
   17.59  \begin{ttdescription}
   17.60 -\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] 
   17.61 -reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
   17.62 -then deletes some formula from the right side of subgoal~$i$, replacing
   17.63 -that formula by~$P$.
   17.64 -
   17.65 -\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] 
   17.66 -reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
   17.67 -then deletes some formula from the left side of the new subgoal $i+1$,
   17.68 -replacing that formula by~$P$.
   17.69 +\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
   17.70 +  applies the cut rule to subgoal~$i$.  It then deletes some formula from the
   17.71 +  right side of subgoal~$i$, replacing that formula by~$P$.
   17.72 +  
   17.73 +\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
   17.74 +  applies the cut rule to subgoal~$i$.  It then deletes some formula from the
   17.75 +  left side of the new subgoal $i+1$, replacing that formula by~$P$.
   17.76  \end{ttdescription}
   17.77  All the structural rules --- cut, contraction, and thinning --- can be
   17.78  applied to particular formulae using {\tt res_inst_tac}.
   17.79 @@ -378,11 +376,11 @@
   17.80  
   17.81  \section{A simple example of classical reasoning} 
   17.82  The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
   17.83 -classical treatment of the existential quantifier.  Classical reasoning
   17.84 -is easy using~{\LK}, as you can see by comparing this proof with the one
   17.85 -given in the FOL manual~\cite{isabelle-ZF}.  From a logical point of view, the
   17.86 -proofs are essentially the same; the key step here is to use \tdx{exR}
   17.87 -rather than the weaker~\tdx{exR_thin}.
   17.88 +classical treatment of the existential quantifier.  Classical reasoning is
   17.89 +easy using~LK, as you can see by comparing this proof with the one given in
   17.90 +the FOL manual~\cite{isabelle-ZF}.  From a logical point of view, the proofs
   17.91 +are essentially the same; the key step here is to use \tdx{exR} rather than
   17.92 +the weaker~\tdx{exR_thin}.
   17.93  \begin{ttbox}
   17.94  Goal "|- EX y. ALL x. P(y)-->P(x)";
   17.95  {\out Level 0}
   17.96 @@ -405,10 +403,10 @@
   17.97  {\out  |- EX y. ALL x. P(y) --> P(x)}
   17.98  {\out  1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
   17.99  \end{ttbox}
  17.100 -Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not
  17.101 -become an assumption;  instead, it moves to the left side.  The
  17.102 -resulting subgoal cannot be instantiated to a basic sequent: the bound
  17.103 -variable~$x$ is not unifiable with the unknown~$\Var{x}$.
  17.104 +Because LK is a sequent calculus, the formula~$P(\Var{x})$ does not become an
  17.105 +assumption; instead, it moves to the left side.  The resulting subgoal cannot
  17.106 +be instantiated to a basic sequent: the bound variable~$x$ is not unifiable
  17.107 +with the unknown~$\Var{x}$.
  17.108  \begin{ttbox}
  17.109  by (resolve_tac [basic] 1);
  17.110  {\out by: tactic failed}
  17.111 @@ -548,10 +546,10 @@
  17.112  Multiple unifiers occur whenever this is resolved against a goal containing
  17.113  more than one conjunction on the left.  
  17.114  
  17.115 -\LK{} exploits this representation of lists.  As an alternative, the
  17.116 -sequent calculus can be formalized using an ordinary representation of
  17.117 -lists, with a logic program for removing a formula from a list.  Amy Felty
  17.118 -has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.
  17.119 +LK exploits this representation of lists.  As an alternative, the sequent
  17.120 +calculus can be formalized using an ordinary representation of lists, with a
  17.121 +logic program for removing a formula from a list.  Amy Felty has applied this
  17.122 +technique using the language $\lambda$Prolog~\cite{felty91a}.
  17.123  
  17.124  Explicit formalization of sequents can be tiresome.  But it gives precise
  17.125  control over contraction and weakening, and is essential to handle relevant
  17.126 @@ -575,10 +573,10 @@
  17.127  rules require a search strategy, such as backtracking.
  17.128  
  17.129  A \textbf{pack} is a pair whose first component is a list of safe rules and
  17.130 -whose second is a list of unsafe rules.  Packs can be extended in an
  17.131 -obvious way to allow reasoning with various collections of rules.  For
  17.132 -clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is
  17.133 -essentially a type synonym:
  17.134 +whose second is a list of unsafe rules.  Packs can be extended in an obvious
  17.135 +way to allow reasoning with various collections of rules.  For clarity, LK
  17.136 +declares \mltydx{pack} as an \ML{} datatype, although is essentially a type
  17.137 +synonym:
  17.138  \begin{ttbox}
  17.139  datatype pack = Pack of thm list * thm list;
  17.140  \end{ttbox}
  17.141 @@ -628,8 +626,7 @@
  17.142  
  17.143  \section{*Proof procedures}\label{sec:sequent-provers}
  17.144  
  17.145 -The \LK{} proof procedure is similar to the classical reasoner
  17.146 -described in 
  17.147 +The LK proof procedure is similar to the classical reasoner described in
  17.148  \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
  17.149              {Chap.\ts\ref{chap:classical}}.  
  17.150  %
    18.1 --- a/doc-src/Logics/Makefile	Mon Aug 28 13:50:24 2000 +0200
    18.2 +++ b/doc-src/Logics/Makefile	Mon Aug 28 13:52:38 2000 +0200
    18.3 @@ -13,7 +13,7 @@
    18.4  
    18.5  NAME = logics
    18.6  FILES = logics.tex preface.tex syntax.tex LK.tex Sequents.tex CTT.tex \
    18.7 -	../proof.sty ../iman.sty ../extra.sty ../manual.bib
    18.8 +	../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    18.9  
   18.10  dvi: $(NAME).dvi
   18.11  
    19.1 --- a/doc-src/Logics/Old_HOL.tex	Mon Aug 28 13:50:24 2000 +0200
    19.2 +++ b/doc-src/Logics/Old_HOL.tex	Mon Aug 28 13:52:38 2000 +0200
    19.3 @@ -3,33 +3,32 @@
    19.4  \index{higher-order logic|(}
    19.5  \index{HOL system@{\sc hol} system}
    19.6  
    19.7 -The theory~\thydx{HOL} implements higher-order logic.
    19.8 -It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
    19.9 -based on Church's original paper~\cite{church40}.  Andrews's
   19.10 -book~\cite{andrews86} is a full description of higher-order logic.
   19.11 -Experience with the {\sc hol} system has demonstrated that higher-order
   19.12 -logic is useful for hardware verification; beyond this, it is widely
   19.13 -applicable in many areas of mathematics.  It is weaker than {\ZF} set
   19.14 -theory but for most applications this does not matter.  If you prefer {\ML}
   19.15 -to Lisp, you will probably prefer \HOL\ to~{\ZF}.
   19.16 +The theory~\thydx{HOL} implements higher-order logic.  It is based on
   19.17 +Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
   19.18 +Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a
   19.19 +full description of higher-order logic.  Experience with the {\sc hol} system
   19.20 +has demonstrated that higher-order logic is useful for hardware verification;
   19.21 +beyond this, it is widely applicable in many areas of mathematics.  It is
   19.22 +weaker than ZF set theory but for most applications this does not matter.  If
   19.23 +you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
   19.24  
   19.25 -Previous releases of Isabelle included a different version of~\HOL, with
   19.26 +Previous releases of Isabelle included a different version of~HOL, with
   19.27  explicit type inference rules~\cite{paulson-COLOG}.  This version no longer
   19.28  exists, but \thydx{ZF} supports a similar style of reasoning.
   19.29  
   19.30 -\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
   19.31 -identifies object-level types with meta-level types, taking advantage of
   19.32 -Isabelle's built-in type checker.  It identifies object-level functions
   19.33 -with meta-level functions, so it uses Isabelle's operations for abstraction
   19.34 -and application.  There is no `apply' operator: function applications are
   19.35 -written as simply~$f(a)$ rather than $f{\tt`}a$.
   19.36 +HOL has a distinct feel, compared with ZF and CTT.  It identifies object-level
   19.37 +types with meta-level types, taking advantage of Isabelle's built-in type
   19.38 +checker.  It identifies object-level functions with meta-level functions, so
   19.39 +it uses Isabelle's operations for abstraction and application.  There is no
   19.40 +`apply' operator: function applications are written as simply~$f(a)$ rather
   19.41 +than $f{\tt`}a$.
   19.42  
   19.43 -These identifications allow Isabelle to support \HOL\ particularly nicely,
   19.44 -but they also mean that \HOL\ requires more sophistication from the user
   19.45 ---- in particular, an understanding of Isabelle's type system.  Beginners
   19.46 -should work with {\tt show_types} set to {\tt true}.  Gain experience by
   19.47 -working in first-order logic before attempting to use higher-order logic.
   19.48 -This chapter assumes familiarity with~{\FOL{}}.
   19.49 +These identifications allow Isabelle to support HOL particularly nicely, but
   19.50 +they also mean that HOL requires more sophistication from the user --- in
   19.51 +particular, an understanding of Isabelle's type system.  Beginners should work
   19.52 +with {\tt show_types} set to {\tt true}.  Gain experience by working in
   19.53 +first-order logic before attempting to use higher-order logic.  This chapter
   19.54 +assumes familiarity with~FOL.
   19.55  
   19.56  
   19.57  \begin{figure} 
   19.58 @@ -115,7 +114,7 @@
   19.59           & | & "EX!~" id~id^* " . " formula
   19.60    \end{array}
   19.61  \]
   19.62 -\caption{Full grammar for \HOL} \label{hol-grammar}
   19.63 +\caption{Full grammar for HOL} \label{hol-grammar}
   19.64  \end{figure} 
   19.65  
   19.66  
   19.67 @@ -140,7 +139,7 @@
   19.68  $\neg(a=b)$.
   19.69  
   19.70  \begin{warn}
   19.71 -  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
   19.72 +  HOL has no if-and-only-if connective; logical equivalence is expressed
   19.73    using equality.  But equality has a high priority, as befitting a
   19.74    relation, while if-and-only-if typically has the lowest priority.  Thus,
   19.75    $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
   19.76 @@ -155,7 +154,7 @@
   19.77  belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
   19.78  over functions.
   19.79  
   19.80 -Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
   19.81 +Types in HOL must be non-empty; otherwise the quantifier rules would be
   19.82  unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
   19.83  
   19.84  \index{type definitions}
   19.85 @@ -178,11 +177,10 @@
   19.86  
   19.87  \subsection{Binders}
   19.88  Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
   19.89 -satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
   19.90 -something, a description is always meaningful, but we do not know its value
   19.91 -unless $P[x]$ defines it uniquely.  We may write descriptions as
   19.92 -\cdx{Eps}($P$) or use the syntax
   19.93 -\hbox{\tt \at $x$.$P[x]$}.
   19.94 +satisfying~$P[a]$, if such exists.  Since all terms in HOL denote something, a
   19.95 +description is always meaningful, but we do not know its value unless $P[x]$
   19.96 +defines it uniquely.  We may write descriptions as \cdx{Eps}($P$) or use the
   19.97 +syntax \hbox{\tt \at $x$.$P[x]$}.
   19.98  
   19.99  Existential quantification is defined by
  19.100  \[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
  19.101 @@ -193,14 +191,14 @@
  19.102  exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
  19.103  
  19.104  \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
  19.105 -Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
  19.106 +Quantifiers have two notations.  As in Gordon's {\sc hol} system, HOL
  19.107  uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
  19.108  existential quantifier must be followed by a space; thus {\tt?x} is an
  19.109  unknown, while \verb'? x.f(x)=y' is a quantification.  Isabelle's usual
  19.110 -notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
  19.111 -available.  Both notations are accepted for input.  The {\ML} reference
  19.112 +notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also available.  Both
  19.113 +notations are accepted for input.  The {\ML} reference
  19.114  \ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
  19.115 -true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
  19.116 +  true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
  19.117  to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
  19.118  
  19.119  All these binders have priority 10. 
  19.120 @@ -212,7 +210,7 @@
  19.121  the constant~\cdx{Let}.  It can be expanded by rewriting with its
  19.122  definition, \tdx{Let_def}.
  19.123  
  19.124 -\HOL\ also defines the basic syntax
  19.125 +HOL also defines the basic syntax
  19.126  \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
  19.127  as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
  19.128    case} and \sdx{of} are reserved words.  However, so far this is mere
  19.129 @@ -259,8 +257,8 @@
  19.130  
  19.131  
  19.132  \section{Rules of inference}
  19.133 -Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
  19.134 -their~{\ML} names.  Some of the rules deserve additional comments:
  19.135 +Figure~\ref{hol-rules} shows the inference rules of~HOL, with their~{\ML}
  19.136 +names.  Some of the rules deserve additional comments:
  19.137  \begin{ttdescription}
  19.138  \item[\tdx{ext}] expresses extensionality of functions.
  19.139  \item[\tdx{iff}] asserts that logically equivalent formulae are
  19.140 @@ -273,14 +271,14 @@
  19.141      shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
  19.142  \end{ttdescription}
  19.143  
  19.144 -\HOL{} follows standard practice in higher-order logic: only a few
  19.145 -connectives are taken as primitive, with the remainder defined obscurely
  19.146 +HOL follows standard practice in higher-order logic: only a few connectives
  19.147 +are taken as primitive, with the remainder defined obscurely
  19.148  (Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
  19.149  corresponding definitions \cite[page~270]{mgordon-hol} using
  19.150 -object-equality~({\tt=}), which is possible because equality in
  19.151 -higher-order logic may equate formulae and even functions over formulae.
  19.152 -But theory~\HOL{}, like all other Isabelle theories, uses
  19.153 -meta-equality~({\tt==}) for definitions.
  19.154 +object-equality~({\tt=}), which is possible because equality in higher-order
  19.155 +logic may equate formulae and even functions over formulae.  But theory~HOL,
  19.156 +like all other Isabelle theories, uses meta-equality~({\tt==}) for
  19.157 +definitions.
  19.158  
  19.159  Some of the rules mention type variables; for
  19.160  example, {\tt refl} mentions the type variable~{\tt'a}.  This allows you to
  19.161 @@ -344,7 +342,7 @@
  19.162  \subcaption{Logical equivalence}
  19.163  
  19.164  \end{ttbox}
  19.165 -\caption{Derived rules for \HOL} \label{hol-lemmas1}
  19.166 +\caption{Derived rules for HOL} \label{hol-lemmas1}
  19.167  \end{figure}
  19.168  
  19.169  
  19.170 @@ -521,8 +519,8 @@
  19.171  \section{A formulation of set theory}
  19.172  Historically, higher-order logic gives a foundation for Russell and
  19.173  Whitehead's theory of classes.  Let us use modern terminology and call them
  19.174 -{\bf sets}, but note that these sets are distinct from those of {\ZF} set
  19.175 -theory, and behave more like {\ZF} classes.
  19.176 +{\bf sets}, but note that these sets are distinct from those of ZF set theory,
  19.177 +and behave more like ZF classes.
  19.178  \begin{itemize}
  19.179  \item
  19.180  Sets are given by predicates over some type~$\sigma$.  Types serve to
  19.181 @@ -534,20 +532,19 @@
  19.182  Although sets may contain other sets as elements, the containing set must
  19.183  have a more complex type.
  19.184  \end{itemize}
  19.185 -Finite unions and intersections have the same behaviour in \HOL\ as they
  19.186 -do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
  19.187 -denoting the universal set for the given type.
  19.188 +Finite unions and intersections have the same behaviour in HOL as they do
  19.189 +in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
  19.190 +universal set for the given type.
  19.191  
  19.192  
  19.193  \subsection{Syntax of set theory}\index{*set type}
  19.194 -\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
  19.195 -essentially the same as $\alpha\To bool$.  The new type is defined for
  19.196 -clarity and to avoid complications involving function types in unification.
  19.197 -Since Isabelle does not support type definitions (as mentioned in
  19.198 -\S\ref{HOL-types}), the isomorphisms between the two types are declared
  19.199 -explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
  19.200 -$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
  19.201 -argument order).
  19.202 +HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially
  19.203 +the same as $\alpha\To bool$.  The new type is defined for clarity and to
  19.204 +avoid complications involving function types in unification.  Since Isabelle
  19.205 +does not support type definitions (as mentioned in \S\ref{HOL-types}), the
  19.206 +isomorphisms between the two types are declared explicitly.  Here they are
  19.207 +natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt
  19.208 +  op :} maps in the other direction (ignoring argument order).
  19.209  
  19.210  Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
  19.211  translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
  19.212 @@ -563,11 +560,11 @@
  19.213    {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
  19.214  \end{eqnarray*}
  19.215  
  19.216 -The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
  19.217 -that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
  19.218 -occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
  19.219 -x.P[x])$.  It defines sets by absolute comprehension, which is impossible
  19.220 -in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
  19.221 +The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type) that
  19.222 +satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences
  19.223 +of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.P[x])$.  It defines
  19.224 +sets by absolute comprehension, which is impossible in~ZF; the type of~$x$
  19.225 +implicitly restricts the comprehension.
  19.226  
  19.227  The set theory defines two {\bf bounded quantifiers}:
  19.228  \begin{eqnarray*}
  19.229 @@ -811,14 +808,13 @@
  19.230  
  19.231  
  19.232  Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
  19.233 -obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
  19.234 -such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
  19.235 -are designed for classical reasoning; the rules \tdx{subsetD},
  19.236 -\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
  19.237 -strictly necessary but yield more natural proofs.  Similarly,
  19.238 -\tdx{equalityCE} supports classical reasoning about extensionality,
  19.239 -after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
  19.240 -proofs pertaining to set theory.
  19.241 +obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such
  19.242 +as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
  19.243 +reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
  19.244 +not strictly necessary but yield more natural proofs.  Similarly,
  19.245 +\tdx{equalityCE} supports classical reasoning about extensionality, after the
  19.246 +fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for proofs pertaining
  19.247 +to set theory.
  19.248  
  19.249  Figure~\ref{hol-fun} presents derived inference rules involving functions.
  19.250  They also include rules for \cdx{Inv}, which is defined in theory~{\tt
  19.251 @@ -905,13 +901,12 @@
  19.252  
  19.253  
  19.254  \section{Generic packages and classical reasoning}
  19.255 -\HOL\ instantiates most of Isabelle's generic packages;
  19.256 -see {\tt HOL/ROOT.ML} for details.
  19.257 +HOL instantiates most of Isabelle's generic packages; see {\tt HOL/ROOT.ML}
  19.258 +for details.
  19.259  \begin{itemize}
  19.260 -\item 
  19.261 -Because it includes a general substitution rule, \HOL\ instantiates the
  19.262 -tactic {\tt hyp_subst_tac}, which substitutes for an equality
  19.263 -throughout a subgoal and its hypotheses.
  19.264 +\item Because it includes a general substitution rule, HOL instantiates the
  19.265 +  tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
  19.266 +  subgoal and its hypotheses.
  19.267  \item 
  19.268  It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
  19.269  simplification set for higher-order logic.  Equality~($=$), which also
  19.270 @@ -921,14 +916,14 @@
  19.271  \item 
  19.272  It instantiates the classical reasoner, as described below. 
  19.273  \end{itemize}
  19.274 -\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
  19.275 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
  19.276 -rule; recall Fig.\ts\ref{hol-lemmas2} above.
  19.277 +HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
  19.278 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
  19.279 +Fig.\ts\ref{hol-lemmas2} above.
  19.280  
  19.281 -The classical reasoner is set up as the structure
  19.282 -{\tt Classical}.  This structure is open, so {\ML} identifiers such
  19.283 -as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
  19.284 -\HOL\ defines the following classical rule sets:
  19.285 +The classical reasoner is set up as the structure {\tt Classical}.  This
  19.286 +structure is open, so {\ML} identifiers such as {\tt step_tac}, {\tt
  19.287 +  fast_tac}, {\tt best_tac}, etc., refer to it.  HOL defines the following
  19.288 +classical rule sets:
  19.289  \begin{ttbox} 
  19.290  prop_cs    : claset
  19.291  HOL_cs     : claset
  19.292 @@ -1075,13 +1070,12 @@
  19.293  called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
  19.294  similar constructions in the context of set theory~\cite{paulson-set-II}.
  19.295  
  19.296 -Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
  19.297 -overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
  19.298 -Isabelle provides no means of verifying that such overloading is sensible;
  19.299 -there is no means of specifying the operators' properties and verifying
  19.300 -that instances of the operators satisfy those properties.  To be safe, the
  19.301 -\HOL\ theory includes no polymorphic axioms asserting general properties of
  19.302 -$<$ and~$\leq$.
  19.303 +Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which overloads
  19.304 +$<$ and $\leq$ on the natural numbers.  As of this writing, Isabelle provides
  19.305 +no means of verifying that such overloading is sensible; there is no means of
  19.306 +specifying the operators' properties and verifying that instances of the
  19.307 +operators satisfy those properties.  To be safe, the HOL theory includes no
  19.308 +polymorphic axioms asserting general properties of $<$ and~$\leq$.
  19.309  
  19.310  Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
  19.311  defines addition, multiplication, subtraction, division, and remainder.
  19.312 @@ -1190,9 +1184,9 @@
  19.313  \subsection{The type constructor for lists, {\tt list}}
  19.314  \index{*list type}
  19.315  
  19.316 -\HOL's definition of lists is an example of an experimental method for
  19.317 -handling recursive data types.  Figure~\ref{hol-list} presents the theory
  19.318 -\thydx{List}: the basic list operations with their types and properties.
  19.319 +HOL's definition of lists is an example of an experimental method for handling
  19.320 +recursive data types.  Figure~\ref{hol-list} presents the theory \thydx{List}:
  19.321 +the basic list operations with their types and properties.
  19.322  
  19.323  The \sdx{case} construct is defined by the following translation:
  19.324  {\dquotes
  19.325 @@ -1740,8 +1734,8 @@
  19.326  proves the two equivalent.  It contains several datatype and inductive
  19.327  definitions, and demonstrates their use.
  19.328  
  19.329 -Directory {\tt HOL/ex} contains other examples and experimental proofs in
  19.330 -{\HOL}.  Here is an overview of the more interesting files.
  19.331 +Directory {\tt HOL/ex} contains other examples and experimental proofs in HOL.
  19.332 +Here is an overview of the more interesting files.
  19.333  \begin{itemize}
  19.334  \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
  19.335    predicate calculus theorems, ranging from simple tautologies to
  19.336 @@ -1770,12 +1764,12 @@
  19.337    as filter, which can compute indefinitely before yielding the next
  19.338    element (if any!) of the lazy list.  A coinduction principle is defined
  19.339    for proving equations on lazy lists.
  19.340 -
  19.341 -\item Theory {\tt PropLog} proves the soundness and completeness of
  19.342 -  classical propositional logic, given a truth table semantics.  The only
  19.343 -  connective is $\imp$.  A Hilbert-style axiom system is specified, and its
  19.344 -  set of theorems defined inductively.  A similar proof in \ZF{} is
  19.345 -  described elsewhere~\cite{paulson-set-II}.
  19.346 +  
  19.347 +\item Theory {\tt PropLog} proves the soundness and completeness of classical
  19.348 +  propositional logic, given a truth table semantics.  The only connective is
  19.349 +  $\imp$.  A Hilbert-style axiom system is specified, and its set of theorems
  19.350 +  defined inductively.  A similar proof in ZF is described
  19.351 +  elsewhere~\cite{paulson-set-II}.
  19.352  
  19.353  \item Theory {\tt Term} develops an experimental recursive type definition;
  19.354    the recursion goes through the type constructor~\tydx{list}.
  19.355 @@ -1804,8 +1798,8 @@
  19.356  of~$\alpha$.  This version states that for every function from $\alpha$ to
  19.357  its powerset, some subset is outside its range.  
  19.358  
  19.359 -The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
  19.360 -the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
  19.361 +The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and the
  19.362 +operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
  19.363  quantified variable so that we may inspect the subset found by the proof.
  19.364  \begin{ttbox}
  19.365  goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
  19.366 @@ -1870,12 +1864,11 @@
  19.367  {\out No subgoals!}
  19.368  \end{ttbox}
  19.369  How much creativity is required?  As it happens, Isabelle can prove this
  19.370 -theorem automatically.  The classical set \ttindex{set_cs} contains rules
  19.371 -for most of the constructs of \HOL's set theory.  We must augment it with
  19.372 -\tdx{equalityCE} to break up set equalities, and then apply best-first
  19.373 -search.  Depth-first search would diverge, but best-first search
  19.374 -successfully navigates through the large search space.
  19.375 -\index{search!best-first}
  19.376 +theorem automatically.  The classical set \ttindex{set_cs} contains rules for
  19.377 +most of the constructs of HOL's set theory.  We must augment it with
  19.378 +\tdx{equalityCE} to break up set equalities, and then apply best-first search.
  19.379 +Depth-first search would diverge, but best-first search successfully navigates
  19.380 +through the large search space.  \index{search!best-first}
  19.381  \begin{ttbox}
  19.382  choplev 0;
  19.383  {\out Level 0}
    20.1 --- a/doc-src/Logics/logics.tex	Mon Aug 28 13:50:24 2000 +0200
    20.2 +++ b/doc-src/Logics/logics.tex	Mon Aug 28 13:52:38 2000 +0200
    20.3 @@ -1,6 +1,6 @@
    20.4  %% $Id$
    20.5  \documentclass[12pt,a4paper]{report}
    20.6 -\usepackage{graphicx,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
    20.7 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
    20.8  
    20.9  %%%STILL NEEDS MODAL, LCF
   20.10  %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
   20.11 @@ -16,8 +16,8 @@
   20.12          With Contributions by Tobias Nipkow and Markus Wenzel%
   20.13   \thanks{Markus Wenzel made numerous improvements.  Sara Kalvala
   20.14      contributed Chap.\ts\ref{chap:sequents}.  Philippe de Groote
   20.15 -   wrote the first version of the logic~\LK{}.  Tobias Nipkow developed
   20.16 -   \LCF{} and~\Cube{}.  Martin Coen developed~\Modal{} with assistance
   20.17 +   wrote the first version of the logic~LK.  Tobias Nipkow developed
   20.18 +   LCF and~Cube.  Martin Coen developed~Modal with assistance
   20.19     from Rajeev Gor\'e.  The research has been funded by the EPSRC
   20.20     (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
   20.21     (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
    21.1 --- a/doc-src/Logics/preface.tex	Mon Aug 28 13:50:24 2000 +0200
    21.2 +++ b/doc-src/Logics/preface.tex	Mon Aug 28 13:52:38 2000 +0200
    21.3 @@ -23,11 +23,11 @@
    21.4  \begin{ttdescription}
    21.5  \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
    21.6    which is the basis of a preliminary method for deriving programs from
    21.7 -  proofs~\cite{coen92}.  It is built upon classical~\FOL{}.
    21.8 +  proofs~\cite{coen92}.  It is built upon classical~FOL.
    21.9   
   21.10  \item[\thydx{LCF}] is a version of Scott's Logic for Computable
   21.11    Functions, which is also implemented by the~{\sc lcf}
   21.12 -  system~\cite{paulson87}.  It is built upon classical~\FOL{}.
   21.13 +  system~\cite{paulson87}.  It is built upon classical~FOL.
   21.14    
   21.15  \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
   21.16    \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.
    22.1 --- a/doc-src/Logics/syntax.tex	Mon Aug 28 13:50:24 2000 +0200
    22.2 +++ b/doc-src/Logics/syntax.tex	Mon Aug 28 13:52:38 2000 +0200
    22.3 @@ -31,16 +31,15 @@
    22.4  becomes syntactically invalid if the brackets are removed.
    22.5  
    22.6  A {\bf binder} is a symbol associated with a constant of type
    22.7 -$(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as
    22.8 -a binder for the constant~$All$, which has type $(\alpha\To o)\To o$.
    22.9 -This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We
   22.10 -can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1.
   22.11 -\ldots \forall x@m.t$; this is possible for any constant provided that
   22.12 -$\tau$ and $\tau'$ are the same type.  \HOL's description operator
   22.13 -$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind
   22.14 -only one variable, except when $\alpha$ is $bool$.  \ZF's bounded
   22.15 -quantifier $\forall x\in A.P(x)$ cannot be declared as a binder
   22.16 -because it has type $[i, i\To o]\To o$.  The syntax for binders allows
   22.17 +$(\sigma\To\tau)\To\tau'$.  For instance, we may declare~$\forall$ as a binder
   22.18 +for the constant~$All$, which has type $(\alpha\To o)\To o$.  This defines the
   22.19 +syntax $\forall x.t$ to mean $All(\lambda x.t)$.  We can also write $\forall
   22.20 +x@1\ldots x@m.t$ to abbreviate $\forall x@1.  \ldots \forall x@m.t$; this is
   22.21 +possible for any constant provided that $\tau$ and $\tau'$ are the same type.
   22.22 +HOL's description operator $\varepsilon x.P\,x$ has type $(\alpha\To
   22.23 +bool)\To\alpha$ and can bind only one variable, except when $\alpha$ is
   22.24 +$bool$.  ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a
   22.25 +binder because it has type $[i, i\To o]\To o$.  The syntax for binders allows
   22.26  type constraints on bound variables, as in
   22.27  \[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]
   22.28  
    23.1 --- a/doc-src/Ref/Makefile	Mon Aug 28 13:50:24 2000 +0200
    23.2 +++ b/doc-src/Ref/Makefile	Mon Aug 28 13:52:38 2000 +0200
    23.3 @@ -15,7 +15,7 @@
    23.4  FILES = ref.tex introduction.tex goals.tex tactic.tex tctical.tex \
    23.5  	thm.tex theories.tex defining.tex syntax.tex substitution.tex \
    23.6  	simplifier.tex classical.tex theory-syntax.tex \
    23.7 -	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
    23.8 +	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    23.9  
   23.10  dvi: $(NAME).dvi
   23.11  
    24.1 --- a/doc-src/Ref/classical.tex	Mon Aug 28 13:50:24 2000 +0200
    24.2 +++ b/doc-src/Ref/classical.tex	Mon Aug 28 13:52:38 2000 +0200
    24.3 @@ -3,12 +3,11 @@
    24.4  \index{classical reasoner|(}
    24.5  \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
    24.6  
    24.7 -Although Isabelle is generic, many users will be working in some
    24.8 -extension of classical first-order logic.  
    24.9 -Isabelle's set theory~{\tt ZF} is built upon theory~\texttt{FOL}, 
   24.10 -while {\HOL} conceptually contains first-order logic as a fragment.
   24.11 -Theorem-proving in predicate logic is undecidable, but many
   24.12 -researchers have developed strategies to assist in this task.
   24.13 +Although Isabelle is generic, many users will be working in some extension of
   24.14 +classical first-order logic.  Isabelle's set theory~ZF is built upon
   24.15 +theory~FOL, while HOL conceptually contains first-order logic as a fragment.
   24.16 +Theorem-proving in predicate logic is undecidable, but many researchers have
   24.17 +developed strategies to assist in this task.
   24.18  
   24.19  Isabelle's classical reasoner is an \ML{} functor that accepts certain
   24.20  information about a logic and delivers a suite of automatic tactics.  Each
   24.21 @@ -52,9 +51,9 @@
   24.22  effectively.  There are many tactics to choose from, including 
   24.23  {\tt Fast_tac} and \texttt{Best_tac}.
   24.24  
   24.25 -We shall first discuss the underlying principles, then present the
   24.26 -classical reasoner.  Finally, we shall see how to instantiate it for new logics.
   24.27 -The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already installed.
   24.28 +We shall first discuss the underlying principles, then present the classical
   24.29 +reasoner.  Finally, we shall see how to instantiate it for new logics.  The
   24.30 +logics FOL, ZF, HOL and HOLCF have it already installed.
   24.31  
   24.32  
   24.33  \section{The sequent calculus}
   24.34 @@ -445,12 +444,11 @@
   24.35  \begin{itemize}
   24.36  \item It does not use the wrapper tacticals described above, such as
   24.37    \ttindex{addss}.
   24.38 -\item It ignores types, which can cause problems in \HOL.  If it applies a rule
   24.39 +\item It ignores types, which can cause problems in HOL.  If it applies a rule
   24.40    whose types are inappropriate, then proof reconstruction will fail.
   24.41  \item It does not perform higher-order unification, as needed by the rule {\tt
   24.42 -    rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}.  There are often
   24.43 -    alternatives to such rules, for example {\tt
   24.44 -    range_eqI} and \texttt{RepFun_eqI}.
   24.45 +    rangeI} in HOL and \texttt{RepFunI} in ZF.  There are often alternatives
   24.46 +  to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
   24.47  \item Function variables may only be applied to parameters of the subgoal.
   24.48  (This restriction arises because the prover does not use higher-order
   24.49  unification.)  If other function variables are present then the prover will
    25.1 --- a/doc-src/Ref/introduction.tex	Mon Aug 28 13:50:24 2000 +0200
    25.2 +++ b/doc-src/Ref/introduction.tex	Mon Aug 28 13:52:38 2000 +0200
    25.3 @@ -34,7 +34,7 @@
    25.4  \({\langle}isabellehome{\rangle}\)/bin/isabelle
    25.5  \end{ttbox}
    25.6  This should start an interactive \ML{} session with the default object-logic
    25.7 -(usually {\HOL}) already pre-loaded.
    25.8 +(usually HOL) already pre-loaded.
    25.9  
   25.10  Subsequently, we assume that the \texttt{isabelle} executable is determined
   25.11  automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
   25.12 @@ -52,7 +52,7 @@
   25.13  isabelle FOL
   25.14  \end{ttbox}
   25.15  This should put you into the world of polymorphic first-order logic (assuming
   25.16 -that an image of {\FOL} has been pre-built).
   25.17 +that an image of FOL has been pre-built).
   25.18  
   25.19  \index{saving your session|bold} Isabelle provides no means of storing
   25.20  theorems or internal proof objects on files.  Theorems are simply part of the
   25.21 @@ -62,7 +62,7 @@
   25.22  \emph{writable} in the first place.  The standard object-logic images are
   25.23  usually read-only, so you have to create a private working copy first.  For
   25.24  example, the following shell command puts you into a writable Isabelle session
   25.25 -of name \texttt{Foo} that initially contains just plain \HOL:
   25.26 +of name \texttt{Foo} that initially contains just plain HOL:
   25.27  \begin{ttbox}
   25.28  isabelle HOL Foo
   25.29  \end{ttbox}
   25.30 @@ -202,7 +202,7 @@
   25.31    
   25.32  \end{ttdescription}
   25.33  
   25.34 -Note that theories of pre-built logic images (e.g.\ {\HOL}) are marked as
   25.35 +Note that theories of pre-built logic images (e.g.\ HOL) are marked as
   25.36  \emph{finished} and cannot be updated any more.  See \S\ref{sec:more-theories}
   25.37  for further information on Isabelle's theory loader.
   25.38  
    26.1 --- a/doc-src/Ref/ref.tex	Mon Aug 28 13:50:24 2000 +0200
    26.2 +++ b/doc-src/Ref/ref.tex	Mon Aug 28 13:52:38 2000 +0200
    26.3 @@ -1,5 +1,5 @@
    26.4  \documentclass[12pt,a4paper]{report}
    26.5 -\usepackage{graphicx,../iman,../extra,../proof,../rail,../pdfsetup}
    26.6 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../pdfsetup}
    26.7  
    26.8  %% $Id$
    26.9  %%\includeonly{}
    27.1 --- a/doc-src/Ref/simp.tex	Mon Aug 28 13:50:24 2000 +0200
    27.2 +++ b/doc-src/Ref/simp.tex	Mon Aug 28 13:52:38 2000 +0200
    27.3 @@ -489,8 +489,8 @@
    27.4  
    27.5  
    27.6  \section{A sample instantiation}
    27.7 -Here is the instantiation of {\tt SIMP_DATA} for {\FOL}.  The code for {\tt
    27.8 -mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
    27.9 +Here is the instantiation of {\tt SIMP_DATA} for FOL.  The code for {\tt
   27.10 +  mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
   27.11  \begin{ttbox}
   27.12  structure FOL_SimpData : SIMP_DATA =
   27.13    struct
    28.1 --- a/doc-src/Ref/simplifier.tex	Mon Aug 28 13:50:24 2000 +0200
    28.2 +++ b/doc-src/Ref/simplifier.tex	Mon Aug 28 13:52:38 2000 +0200
    28.3 @@ -3,12 +3,11 @@
    28.4  \label{chap:simplification}
    28.5  \index{simplification|(}
    28.6  
    28.7 -This chapter describes Isabelle's generic simplification package.  It
    28.8 -performs conditional and unconditional rewriting and uses contextual
    28.9 -information (`local assumptions').  It provides several general hooks,
   28.10 -which can provide automatic case splits during rewriting, for example.
   28.11 -The simplifier is already set up for many of Isabelle's logics: \FOL,
   28.12 -\ZF, \HOL, \HOLCF.
   28.13 +This chapter describes Isabelle's generic simplification package.  It performs
   28.14 +conditional and unconditional rewriting and uses contextual information
   28.15 +(`local assumptions').  It provides several general hooks, which can provide
   28.16 +automatic case splits during rewriting, for example.  The simplifier is
   28.17 +already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF.
   28.18  
   28.19  The first section is a quick introduction to the simplifier that
   28.20  should be sufficient to get started.  The later sections explain more
   28.21 @@ -71,9 +70,9 @@
   28.22  
   28.23  \medskip
   28.24  
   28.25 -As an example, consider the theory of arithmetic in \HOL.  The (rather
   28.26 -trivial) goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call
   28.27 -of \texttt{Simp_tac} as follows:
   28.28 +As an example, consider the theory of arithmetic in HOL.  The (rather trivial)
   28.29 +goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call of
   28.30 +\texttt{Simp_tac} as follows:
   28.31  \begin{ttbox}
   28.32  context Arith.thy;
   28.33  Goal "0 + (x + 0) = x + 0 + 0";
   28.34 @@ -181,11 +180,11 @@
   28.35  
   28.36  \end{ttdescription}
   28.37  
   28.38 -When a new theory is built, its implicit simpset is initialized by the
   28.39 -union of the respective simpsets of its parent theories.  In addition,
   28.40 -certain theory definition constructs (e.g.\ \ttindex{datatype} and
   28.41 -\ttindex{primrec} in \HOL) implicitly augment the current simpset.
   28.42 -Ordinary definitions are not added automatically!
   28.43 +When a new theory is built, its implicit simpset is initialized by the union
   28.44 +of the respective simpsets of its parent theories.  In addition, certain
   28.45 +theory definition constructs (e.g.\ \ttindex{datatype} and \ttindex{primrec}
   28.46 +in HOL) implicitly augment the current simpset.  Ordinary definitions are not
   28.47 +added automatically!
   28.48  
   28.49  It is up the user to manipulate the current simpset further by
   28.50  explicitly adding or deleting theorems and simplification procedures.
   28.51 @@ -253,12 +252,11 @@
   28.52  \end{ttbox}
   28.53  \begin{ttdescription}
   28.54    
   28.55 -\item[\ttindexbold{empty_ss}] is the empty simpset.  This is not very
   28.56 -  useful under normal circumstances because it doesn't contain
   28.57 -  suitable tactics (subgoaler etc.).  When setting up the simplifier
   28.58 -  for a particular object-logic, one will typically define a more
   28.59 -  appropriate ``almost empty'' simpset.  For example, in \HOL\ this is
   28.60 -  called \ttindexbold{HOL_basic_ss}.
   28.61 +\item[\ttindexbold{empty_ss}] is the empty simpset.  This is not very useful
   28.62 +  under normal circumstances because it doesn't contain suitable tactics
   28.63 +  (subgoaler etc.).  When setting up the simplifier for a particular
   28.64 +  object-logic, one will typically define a more appropriate ``almost empty''
   28.65 +  simpset.  For example, in HOL this is called \ttindexbold{HOL_basic_ss}.
   28.66    
   28.67  \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$
   28.68    and $ss@2$ by building the union of their respective rewrite rules,
   28.69 @@ -1077,12 +1075,11 @@
   28.70  
   28.71  \subsection{Example: sums of natural numbers}
   28.72  
   28.73 -This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}).
   28.74 -Theory \thydx{Arith} contains natural numbers arithmetic.  Its
   28.75 -associated simpset contains many arithmetic laws including
   28.76 -distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list
   28.77 -consisting of the A, C and LC laws for~$+$ on type \texttt{nat}.  Let
   28.78 -us prove the theorem
   28.79 +This example is again set in HOL (see \texttt{HOL/ex/NatSum}).  Theory
   28.80 +\thydx{Arith} contains natural numbers arithmetic.  Its associated simpset
   28.81 +contains many arithmetic laws including distributivity of~$\times$ over~$+$,
   28.82 +while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on
   28.83 +type \texttt{nat}.  Let us prove the theorem
   28.84  \[ \sum@{i=1}^n i = n\times(n+1)/2. \]
   28.85  %
   28.86  A functional~\texttt{sum} represents the summation operator under the
   28.87 @@ -1216,12 +1213,11 @@
   28.88  \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external
   28.89  model checker syntax).
   28.90    
   28.91 -The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an
   28.92 -operator \texttt{split} together with some concrete syntax supporting
   28.93 -$\lambda\,(x,y).b$ abstractions.  Assume that we would like to offer a
   28.94 -tactic that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of
   28.95 -some pair type) to $\lambda\,(x,y).f\,(x,y)$.  The corresponding rule
   28.96 -is:
   28.97 +The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator
   28.98 +\texttt{split} together with some concrete syntax supporting
   28.99 +$\lambda\,(x,y).b$ abstractions.  Assume that we would like to offer a tactic
  28.100 +that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type)
  28.101 +to $\lambda\,(x,y).f\,(x,y)$.  The corresponding rule is:
  28.102  \begin{ttbox}
  28.103  pair_eta_expand:  (f::'a*'b=>'c) = (\%(x, y). f (x, y))
  28.104  \end{ttbox}
  28.105 @@ -1298,7 +1294,7 @@
  28.106  We first prove lots of standard rewrite rules about the logical
  28.107  connectives.  These include cancellation and associative laws.  We
  28.108  define a function that echoes the desired law and then supplies it the
  28.109 -prover for intuitionistic \FOL:
  28.110 +prover for intuitionistic FOL:
  28.111  \begin{ttbox}
  28.112  fun int_prove_fun s = 
  28.113   (writeln s;  
  28.114 @@ -1437,12 +1433,11 @@
  28.115  val triv_rls = [TrueI,refl,iff_refl,notFalseI];
  28.116  \end{ttbox}
  28.117  %
  28.118 -The basic simpset for intuitionistic \FOL{} is
  28.119 -\ttindexbold{FOL_basic_ss}.  It preprocess rewrites using {\tt
  28.120 -  gen_all}, \texttt{atomize} and \texttt{mk_eq}.  It solves simplified
  28.121 -subgoals using \texttt{triv_rls} and assumptions, and by detecting
  28.122 -contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals of
  28.123 -conditional rewrites.
  28.124 +The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}.  It
  28.125 +preprocess rewrites using {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
  28.126 +It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
  28.127 +detecting contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals
  28.128 +of conditional rewrites.
  28.129  
  28.130  Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
  28.131  In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
    29.1 --- a/doc-src/Ref/substitution.tex	Mon Aug 28 13:50:24 2000 +0200
    29.2 +++ b/doc-src/Ref/substitution.tex	Mon Aug 28 13:52:38 2000 +0200
    29.3 @@ -61,7 +61,7 @@
    29.4  eresolve_tac [subst] \(i\)    {\rm or}    eresolve_tac [ssubst] \(i\){\it.}
    29.5  \end{ttbox}
    29.6  
    29.7 -Logics \HOL, {\FOL} and {\ZF} define the tactic \ttindexbold{stac} by
    29.8 +Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by
    29.9  \begin{ttbox} 
   29.10  fun stac eqth = CHANGED o rtac (eqth RS ssubst);
   29.11  \end{ttbox}
    30.1 --- a/doc-src/Ref/syntax.tex	Mon Aug 28 13:50:24 2000 +0200
    30.2 +++ b/doc-src/Ref/syntax.tex	Mon Aug 28 13:52:38 2000 +0200
    30.3 @@ -688,11 +688,11 @@
    30.4  \section{Translation functions} \label{sec:tr_funs}
    30.5  \index{translations|(}
    30.6  %
    30.7 -This section describes the translation function mechanism.  By writing
    30.8 -\ML{} functions, you can do almost everything to terms or \AST{}s
    30.9 -during parsing and printing.  The logic \LK\ is a good example of
   30.10 -sophisticated transformations between internal and external
   30.11 -representations of sequents; here, macros would be useless.
   30.12 +This section describes the translation function mechanism.  By writing \ML{}
   30.13 +functions, you can do almost everything to terms or \AST{}s during parsing and
   30.14 +printing.  The logic LK is a good example of sophisticated transformations
   30.15 +between internal and external representations of sequents; here, macros would
   30.16 +be useless.
   30.17  
   30.18  A full understanding of translations requires some familiarity
   30.19  with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
    31.1 --- a/doc-src/Ref/tactic.tex	Mon Aug 28 13:50:24 2000 +0200
    31.2 +++ b/doc-src/Ref/tactic.tex	Mon Aug 28 13:52:38 2000 +0200
    31.3 @@ -422,9 +422,9 @@
    31.4  flexflex_tac          : tactic
    31.5  \end{ttbox}
    31.6  \begin{ttdescription}
    31.7 -\item[\ttindexbold{distinct_subgoals_tac}]  
    31.8 -  removes duplicate subgoals from a proof state.  (These arise especially
    31.9 -  in \ZF{}, where the subgoals are essentially type constraints.)
   31.10 +\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a
   31.11 +  proof state.  (These arise especially in ZF, where the subgoals are
   31.12 +  essentially type constraints.)
   31.13  
   31.14  \item[\ttindexbold{prune_params_tac}]  
   31.15    removes unused parameters from all subgoals of the proof state.  It works
    32.1 --- a/doc-src/Ref/theories.tex	Mon Aug 28 13:50:24 2000 +0200
    32.2 +++ b/doc-src/Ref/theories.tex	Mon Aug 28 13:52:38 2000 +0200
    32.3 @@ -3,12 +3,12 @@
    32.4  
    32.5  \chapter{Theories, Terms and Types} \label{theories}
    32.6  \index{theories|(}\index{signatures|bold}
    32.7 -\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the
    32.8 -syntax, declarations and axioms of a mathematical development.  They
    32.9 -are built, starting from the {\Pure} or {\CPure} theory, by extending
   32.10 -and merging existing theories.  They have the \ML\ type
   32.11 -\mltydx{theory}.  Theory operations signal errors by raising exception
   32.12 -\xdx{THEORY}, returning a message and a list of theories.
   32.13 +\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the syntax,
   32.14 +declarations and axioms of a mathematical development.  They are built,
   32.15 +starting from the Pure or CPure theory, by extending and merging existing
   32.16 +theories.  They have the \ML\ type \mltydx{theory}.  Theory operations signal
   32.17 +errors by raising exception \xdx{THEORY}, returning a message and a list of
   32.18 +theories.
   32.19  
   32.20  Signatures, which contain information about sorts, types, constants and
   32.21  syntax, have the \ML\ type~\mltydx{Sign.sg}.  For identification, each
   32.22 @@ -715,9 +715,9 @@
   32.23  \item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
   32.24  is the \textbf{application} of~$t$ to~$u$.
   32.25  \end{ttdescription}
   32.26 -Application is written as an infix operator to aid readability.
   32.27 -Here is an \ML\ pattern to recognize \FOL{} formulae of
   32.28 -the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
   32.29 +Application is written as an infix operator to aid readability.  Here is an
   32.30 +\ML\ pattern to recognize FOL formulae of the form~$A\imp B$, binding the
   32.31 +subformulae to~$A$ and~$B$:
   32.32  \begin{ttbox}
   32.33  Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
   32.34  \end{ttbox}
    33.1 --- a/doc-src/Ref/theory-syntax.tex	Mon Aug 28 13:50:24 2000 +0200
    33.2 +++ b/doc-src/Ref/theory-syntax.tex	Mon Aug 28 13:52:38 2000 +0200
    33.3 @@ -5,10 +5,10 @@
    33.4  
    33.5  \chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
    33.6  
    33.7 -Below we present the full syntax of theory definition files as
    33.8 -provided by {\Pure} Isabelle --- object-logics may add their own
    33.9 -sections.  \S\ref{sec:ref-defining-theories} explains the meanings of
   33.10 -these constructs.  The syntax obeys the following conventions:
   33.11 +Below we present the full syntax of theory definition files as provided by
   33.12 +Pure Isabelle --- object-logics may add their own sections.
   33.13 +\S\ref{sec:ref-defining-theories} explains the meanings of these constructs.
   33.14 +The syntax obeys the following conventions:
   33.15  \begin{itemize}
   33.16  \item {\tt Typewriter font} denotes terminal symbols.
   33.17    
    34.1 --- a/doc-src/System/Makefile	Mon Aug 28 13:50:24 2000 +0200
    34.2 +++ b/doc-src/System/Makefile	Mon Aug 28 13:52:38 2000 +0200
    34.3 @@ -13,7 +13,7 @@
    34.4  
    34.5  NAME = system
    34.6  FILES = system.tex basics.tex misc.tex fonts.tex present.tex \
    34.7 -	../iman.sty ../extra.sty ../manual.bib
    34.8 +	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    34.9  
   34.10  dvi: $(NAME).dvi
   34.11  
    35.1 --- a/doc-src/System/fonts.tex	Mon Aug 28 13:50:24 2000 +0200
    35.2 +++ b/doc-src/System/fonts.tex	Mon Aug 28 13:52:38 2000 +0200
    35.3 @@ -4,8 +4,8 @@
    35.4  \chapter{Fonts and character encodings}
    35.5  
    35.6  Using the print mode mechanism of Isabelle, variant forms of output become
    35.7 -very easy. As the canonical application of this feature, {\Pure} and major
    35.8 -object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional input and output of
    35.9 +very easy. As the canonical application of this feature, Pure and major
   35.10 +object-logics (FOL, ZF, HOL, HOLCF) support optional input and output of
   35.11  proper mathematical symbols as built-in option.
   35.12  
   35.13  Symbolic output is enabled by activating the ``\ttindex{symbols}'' print mode.
    36.1 --- a/doc-src/System/present.tex	Mon Aug 28 13:50:24 2000 +0200
    36.2 +++ b/doc-src/System/present.tex	Mon Aug 28 13:52:38 2000 +0200
    36.3 @@ -38,7 +38,7 @@
    36.4  
    36.5  In order to let Isabelle generate theory browsing information, simply append
    36.6  ``\texttt{-i true}'' to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before
    36.7 -making a logic.  For example, in order to do this for {\FOL}, add this to your
    36.8 +making a logic.  For example, in order to do this for FOL, add this to your
    36.9  Isabelle settings file
   36.10  \begin{ttbox}
   36.11  ISABELLE_USEDIR_OPTIONS="-i true"
   36.12 @@ -87,8 +87,8 @@
   36.13  isatool usedir -i true HOL Foo
   36.14  \end{ttbox}
   36.15  This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
   36.16 -to load all your theories, and {\HOL} is your parent logic image.  Ideally,
   36.17 -theory browser information would have been generated for {\HOL} already.
   36.18 +to load all your theories, and HOL is your parent logic image.  Ideally,
   36.19 +theory browser information would have been generated for HOL already.
   36.20  
   36.21  Alternatively, one may specify an external link to an existing body of HTML
   36.22  data by giving \texttt{usedir} a \texttt{-P} option like this:
   36.23 @@ -499,7 +499,7 @@
   36.24  \medskip Any \texttt{usedir} session is named by some \emph{session
   36.25    identifier}. These accumulate, documenting the way sessions depend on
   36.26  others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
   36.27 -examples of {\FOL}, which in turn is built upon {\Pure}.
   36.28 +examples of FOL, which in turn is built upon Pure.
   36.29  
   36.30  The current session's identifier is by default just the base name of the
   36.31  \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in
    37.1 --- a/doc-src/System/system.tex	Mon Aug 28 13:50:24 2000 +0200
    37.2 +++ b/doc-src/System/system.tex	Mon Aug 28 13:52:38 2000 +0200
    37.3 @@ -2,7 +2,7 @@
    37.4  %% $Id$
    37.5  
    37.6  \documentclass[12pt,a4paper]{report}
    37.7 -\usepackage{graphicx,../iman,../extra,../pdfsetup}
    37.8 +\usepackage{graphicx,../iman,../extra,../ttbox,../pdfsetup}
    37.9  
   37.10  
   37.11  \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
    38.1 --- a/doc-src/Tutorial/Makefile	Mon Aug 28 13:50:24 2000 +0200
    38.2 +++ b/doc-src/Tutorial/Makefile	Mon Aug 28 13:52:38 2000 +0200
    38.3 @@ -13,7 +13,7 @@
    38.4  
    38.5  NAME = tutorial
    38.6  FILES = tutorial.tex basics.tex fp.tex appendix.tex \
    38.7 -	../iman.sty ttbox.sty extra.sty
    38.8 +	../iman.sty ../ttbox.sty ../extra.sty
    38.9  
   38.10  dvi: $(NAME).dvi
   38.11  
    39.1 --- a/doc-src/Tutorial/extra.sty	Mon Aug 28 13:50:24 2000 +0200
    39.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    39.3 @@ -1,29 +0,0 @@
    39.4 -% extra.sty : Isabelle Manual extra macros for non-Springer version
    39.5 -%
    39.6 -\typeout{Document Style extra. Released 17/2/94, version of 22/8/00}
    39.7 -
    39.8 -\usepackage{ttbox}
    39.9 -{\obeylines\gdef\ttbreak
   39.10 -{\allowbreak}}
   39.11 -
   39.12 -%%Euro-style date: 20 September 1955
   39.13 -\def\today{\number\day\space\ifcase\month\or
   39.14 -January\or February\or March\or April\or May\or June\or
   39.15 -July\or August\or September\or October\or November\or December\fi
   39.16 -\space\number\year}
   39.17 -
   39.18 -%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
   39.19 -\newcommand\clearfirst{\clearpage\ifodd\c@page\else
   39.20 -    \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
   39.21 -    \pagenumbering{arabic}}
   39.22 -
   39.23 -%%%Ruled chapter headings 
   39.24 -\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf 
   39.25 -   #1 \vskip 14pt\hrule height1pt}
   39.26 -\def\@makechapterhead#1{ { \parindent 0pt 
   39.27 - \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par 
   39.28 - \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
   39.29 -
   39.30 -\def\@makeschapterhead#1{ { \parindent 0pt \raggedright 
   39.31 - \@rulehead{#1} \par \nobreak \vskip 40pt } }
   39.32 -
    40.1 --- a/doc-src/Tutorial/ttbox.sty	Mon Aug 28 13:50:24 2000 +0200
    40.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    40.3 @@ -1,20 +0,0 @@
    40.4 -\ProvidesPackage{ttbox}[1997/06/25]
    40.5 -\RequirePackage{alltt}
    40.6 -
    40.7 -%%%Boxed terminal sessions
    40.8 -
    40.9 -%Redefines \{ and \} to be in \tt font and \| to make a BACKSLASH
   40.10 -\def\ttbraces{\chardef\{=`\{\chardef\}=`\}\chardef\|=`\\}
   40.11 -
   40.12 -%Restores % as the comment character (especially, to suppress line breaks)
   40.13 -\newcommand\comments{\catcode`\%=14\relax}
   40.14 -
   40.15 -%alltt* environment: like alltt but smaller, and with \{ \} and \| as in ttbox
   40.16 -\newenvironment{alltt*}{\begin{alltt}\footnotesize\ttbraces}{\end{alltt}}
   40.17 -
   40.18 -%Indented alltt* environment with small point size
   40.19 -%NO LINE BREAKS are allowed unless \pagebreak appears at START of a line
   40.20 -\newenvironment{ttbox}{\begin{quote}\samepage\begin{alltt*}}%
   40.21 -                      {\end{alltt*}\end{quote}}
   40.22 -
   40.23 -\endinput
    41.1 --- a/doc-src/Tutorial/tutorial.tex	Mon Aug 28 13:50:24 2000 +0200
    41.2 +++ b/doc-src/Tutorial/tutorial.tex	Mon Aug 28 13:52:38 2000 +0200
    41.3 @@ -1,5 +1,5 @@
    41.4  \documentclass[11pt,a4paper]{report}
    41.5 -\usepackage{latexsym,verbatim,graphicx,../iman,extra,../pdfsetup}
    41.6 +\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,../pdfsetup}
    41.7  
    41.8  \newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions
    41.9  
    42.1 --- a/doc-src/TutorialI/Makefile	Mon Aug 28 13:50:24 2000 +0200
    42.2 +++ b/doc-src/TutorialI/Makefile	Mon Aug 28 13:52:38 2000 +0200
    42.3 @@ -13,7 +13,7 @@
    42.4  
    42.5  NAME = tutorial
    42.6  FILES = tutorial.tex basics.tex fp.tex appendix.tex \
    42.7 -	../iman.sty ttbox.sty extra.sty \
    42.8 +	../iman.sty ../ttbox.sty ../extra.sty \
    42.9  	isabelle.sty isabellesym.sty ../pdfsetup.sty
   42.10  
   42.11  dvi: $(NAME).dvi
    43.1 --- a/doc-src/TutorialI/extra.sty	Mon Aug 28 13:50:24 2000 +0200
    43.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    43.3 @@ -1,29 +0,0 @@
    43.4 -% extra.sty : Isabelle Manual extra macros for non-Springer version
    43.5 -%
    43.6 -\typeout{Document Style extra. Released 17/2/94, version of 22/8/00}
    43.7 -
    43.8 -\usepackage{ttbox}
    43.9 -{\obeylines\gdef\ttbreak
   43.10 -{\allowbreak}}
   43.11 -
   43.12 -%%Euro-style date: 20 September 1955
   43.13 -\def\today{\number\day\space\ifcase\month\or
   43.14 -January\or February\or March\or April\or May\or June\or
   43.15 -July\or August\or September\or October\or November\or December\fi
   43.16 -\space\number\year}
   43.17 -
   43.18 -%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
   43.19 -\newcommand\clearfirst{\clearpage\ifodd\c@page\else
   43.20 -    \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
   43.21 -    \pagenumbering{arabic}}
   43.22 -
   43.23 -%%%Ruled chapter headings 
   43.24 -\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf 
   43.25 -   #1 \vskip 14pt\hrule height1pt}
   43.26 -\def\@makechapterhead#1{ { \parindent 0pt 
   43.27 - \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par 
   43.28 - \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
   43.29 -
   43.30 -\def\@makeschapterhead#1{ { \parindent 0pt \raggedright 
   43.31 - \@rulehead{#1} \par \nobreak \vskip 40pt } }
   43.32 -
    44.1 --- a/doc-src/TutorialI/ttbox.sty	Mon Aug 28 13:50:24 2000 +0200
    44.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    44.3 @@ -1,20 +0,0 @@
    44.4 -\ProvidesPackage{ttbox}[1997/06/25]
    44.5 -\RequirePackage{alltt}
    44.6 -
    44.7 -%%%Boxed terminal sessions
    44.8 -
    44.9 -%Redefines \{ and \} to be in \tt font and \| to make a BACKSLASH
   44.10 -\def\ttbraces{\chardef\{=`\{\chardef\}=`\}\chardef\|=`\\}
   44.11 -
   44.12 -%Restores % as the comment character (especially, to suppress line breaks)
   44.13 -\newcommand\comments{\catcode`\%=14\relax}
   44.14 -
   44.15 -%alltt* environment: like alltt but smaller, and with \{ \} and \| as in ttbox
   44.16 -\newenvironment{alltt*}{\begin{alltt}\footnotesize\ttbraces}{\end{alltt}}
   44.17 -
   44.18 -%Indented alltt* environment with small point size
   44.19 -%NO LINE BREAKS are allowed unless \pagebreak appears at START of a line
   44.20 -\newenvironment{ttbox}{\begin{quote}\samepage\begin{alltt*}}%
   44.21 -                      {\end{alltt*}\end{quote}}
   44.22 -
   44.23 -\endinput
    45.1 --- a/doc-src/TutorialI/tutorial.tex	Mon Aug 28 13:50:24 2000 +0200
    45.2 +++ b/doc-src/TutorialI/tutorial.tex	Mon Aug 28 13:52:38 2000 +0200
    45.3 @@ -1,7 +1,7 @@
    45.4  % pr(latex xsymbols symbols)
    45.5  \documentclass[11pt,a4paper]{report}
    45.6  \usepackage{isabelle,isabellesym}
    45.7 -\usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}
    45.8 +\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
    45.9  \usepackage{../pdfsetup}    %last package!
   45.10  
   45.11  \newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions
    46.1 --- a/doc-src/ZF/FOL.tex	Mon Aug 28 13:50:24 2000 +0200
    46.2 +++ b/doc-src/ZF/FOL.tex	Mon Aug 28 13:52:38 2000 +0200
    46.3 @@ -192,7 +192,7 @@
    46.4  
    46.5  
    46.6  \section{Generic packages}
    46.7 -\FOL{} instantiates most of Isabelle's generic packages.
    46.8 +FOL instantiates most of Isabelle's generic packages.
    46.9  \begin{itemize}
   46.10  \item 
   46.11  It instantiates the simplifier.  Both equality ($=$) and the biconditional
   46.12 @@ -210,9 +210,9 @@
   46.13  It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
   46.14  for details. 
   46.15  
   46.16 -\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
   46.17 -  for an equality throughout a subgoal and its hypotheses.  This tactic uses
   46.18 -  \FOL's general substitution rule.
   46.19 +\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
   46.20 +  an equality throughout a subgoal and its hypotheses.  This tactic uses FOL's
   46.21 +  general substitution rule.
   46.22  \end{itemize}
   46.23  
   46.24  \begin{warn}\index{simplification!of conjunctions}%
   46.25 @@ -331,10 +331,10 @@
   46.26  the rule
   46.27  $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
   46.28  \noindent
   46.29 -Natural deduction in classical logic is not really all that natural.
   46.30 -{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
   46.31 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
   46.32 -rule (see Fig.\ts\ref{fol-cla-derived}).
   46.33 +Natural deduction in classical logic is not really all that natural.  FOL
   46.34 +derives classical introduction rules for $\disj$ and~$\exists$, as well as
   46.35 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
   46.36 +Fig.\ts\ref{fol-cla-derived}).
   46.37  
   46.38  The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
   46.39  Best_tac} refer to the default claset (\texttt{claset()}), which works for most
   46.40 @@ -897,8 +897,8 @@
   46.41  while~$R$ and~$A$ are true.  This truth assignment reduces the main goal to
   46.42  $true\bimp false$, which is of course invalid.
   46.43  
   46.44 -We can repeat this analysis by expanding definitions, using just
   46.45 -the rules of {\FOL}:
   46.46 +We can repeat this analysis by expanding definitions, using just the rules of
   46.47 +FOL:
   46.48  \begin{ttbox}
   46.49  choplev 0;
   46.50  {\out Level 0}
    47.1 --- a/doc-src/ZF/Makefile	Mon Aug 28 13:50:24 2000 +0200
    47.2 +++ b/doc-src/ZF/Makefile	Mon Aug 28 13:52:38 2000 +0200
    47.3 @@ -13,7 +13,7 @@
    47.4  
    47.5  NAME = logics-ZF
    47.6  FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex \
    47.7 -	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
    47.8 +	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    47.9  
   47.10  dvi: $(NAME).dvi
   47.11  
    48.1 --- a/doc-src/ZF/ZF.tex	Mon Aug 28 13:50:24 2000 +0200
    48.2 +++ b/doc-src/ZF/ZF.tex	Mon Aug 28 13:52:38 2000 +0200
    48.3 @@ -23,10 +23,9 @@
    48.4  provides a streamlined syntax for defining primitive recursive functions over
    48.5  datatypes. 
    48.6  
    48.7 -Because {\ZF} is an extension of {\FOL}, it provides the same
    48.8 -packages, namely \texttt{hyp_subst_tac}, the simplifier, and the
    48.9 -classical reasoner.  The default simpset and claset are usually
   48.10 -satisfactory.
   48.11 +Because ZF is an extension of FOL, it provides the same packages, namely
   48.12 +\texttt{hyp_subst_tac}, the simplifier, and the classical reasoner.  The
   48.13 +default simpset and claset are usually satisfactory.
   48.14  
   48.15  Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
   48.16  less formally than this chapter.  Isabelle employs a novel treatment of
   48.17 @@ -94,7 +93,7 @@
   48.18  \begin{center}
   48.19  \index{*"`"` symbol}
   48.20  \index{*"-"`"` symbol}
   48.21 -\index{*"` symbol}\index{function applications!in \ZF}
   48.22 +\index{*"` symbol}\index{function applications!in ZF}
   48.23  \index{*"- symbol}
   48.24  \index{*": symbol}
   48.25  \index{*"<"= symbol}
   48.26 @@ -111,7 +110,7 @@
   48.27  \end{tabular}
   48.28  \end{center}
   48.29  \subcaption{Infixes}
   48.30 -\caption{Constants of {\ZF}} \label{zf-constants}
   48.31 +\caption{Constants of ZF} \label{zf-constants}
   48.32  \end{figure} 
   48.33  
   48.34  
   48.35 @@ -125,10 +124,10 @@
   48.36  bounded quantifiers.  In most other respects, Isabelle implements precisely
   48.37  Zermelo-Fraenkel set theory.
   48.38  
   48.39 -Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
   48.40 +Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while
   48.41  Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   48.42 -Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   48.43 -the constructs of \FOL.
   48.44 +Figure~\ref{zf-syntax} presents the full grammar for set theory, including the
   48.45 +constructs of FOL.
   48.46  
   48.47  Local abbreviations can be introduced by a \texttt{let} construct whose
   48.48  syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into
   48.49 @@ -136,7 +135,7 @@
   48.50  definition, \tdx{Let_def}.
   48.51  
   48.52  Apart from \texttt{let}, set theory does not use polymorphism.  All terms in
   48.53 -{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
   48.54 +ZF have type~\tydx{i}, which is the type of individuals and has class~{\tt
   48.55    term}.  The type of first-order formulae, remember, is~\textit{o}.
   48.56  
   48.57  Infix operators include binary union and intersection ($A\un B$ and
   48.58 @@ -167,15 +166,15 @@
   48.59  abbreviates the nest of pairs\par\nobreak
   48.60  \centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
   48.61  
   48.62 -In {\ZF}, a function is a set of pairs.  A {\ZF} function~$f$ is simply an
   48.63 -individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
   48.64 -say $i\To i$.  The infix operator~{\tt`} denotes the application of a
   48.65 -function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The
   48.66 -syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
   48.67 +In ZF, a function is a set of pairs.  A ZF function~$f$ is simply an
   48.68 +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
   48.69 +$i\To i$.  The infix operator~{\tt`} denotes the application of a function set
   48.70 +to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The syntax for image
   48.71 +is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
   48.72  
   48.73  
   48.74  \begin{figure} 
   48.75 -\index{lambda abs@$\lambda$-abstractions!in \ZF}
   48.76 +\index{lambda abs@$\lambda$-abstractions!in ZF}
   48.77  \index{*"-"> symbol}
   48.78  \index{*"* symbol}
   48.79  \begin{center} \footnotesize\tt\frenchspacing
   48.80 @@ -215,7 +214,7 @@
   48.81          \rm bounded $\exists$
   48.82  \end{tabular}
   48.83  \end{center}
   48.84 -\caption{Translations for {\ZF}} \label{zf-trans}
   48.85 +\caption{Translations for ZF} \label{zf-trans}
   48.86  \end{figure} 
   48.87  
   48.88  
   48.89 @@ -264,7 +263,7 @@
   48.90           & | & "EX!~" id~id^* " . " formula
   48.91    \end{array}
   48.92  \]
   48.93 -\caption{Full grammar for {\ZF}} \label{zf-syntax}
   48.94 +\caption{Full grammar for ZF} \label{zf-syntax}
   48.95  \end{figure} 
   48.96  
   48.97  
   48.98 @@ -321,14 +320,13 @@
   48.99  no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
  48.100  abbreviations in parsing and uses them whenever possible for printing.
  48.101  
  48.102 -\index{*THE symbol} 
  48.103 -As mentioned above, whenever the axioms assert the existence and uniqueness
  48.104 -of a set, Isabelle's set theory declares a constant for that set.  These
  48.105 -constants can express the {\bf definite description} operator~$\iota
  48.106 -x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.
  48.107 -Since all terms in {\ZF} denote something, a description is always
  48.108 -meaningful, but we do not know its value unless $P[x]$ defines it uniquely.
  48.109 -Using the constant~\cdx{The}, we may write descriptions as {\tt
  48.110 +\index{*THE symbol} As mentioned above, whenever the axioms assert the
  48.111 +existence and uniqueness of a set, Isabelle's set theory declares a constant
  48.112 +for that set.  These constants can express the {\bf definite description}
  48.113 +operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$,
  48.114 +if such exists.  Since all terms in ZF denote something, a description is
  48.115 +always meaningful, but we do not know its value unless $P[x]$ defines it
  48.116 +uniquely.  Using the constant~\cdx{The}, we may write descriptions as {\tt
  48.117    The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}.
  48.118  
  48.119  \index{*lam symbol}
  48.120 @@ -385,7 +383,7 @@
  48.121  \tdx{Diff_def}     A - B    == {\ttlbrace}x:A . x~:B{\ttrbrace}
  48.122  \subcaption{Union, intersection, difference}
  48.123  \end{ttbox}
  48.124 -\caption{Rules and axioms of {\ZF}} \label{zf-rules}
  48.125 +\caption{Rules and axioms of ZF} \label{zf-rules}
  48.126  \end{figure}
  48.127  
  48.128  
  48.129 @@ -417,7 +415,7 @@
  48.130  \tdx{restrict_def}   restrict(f,A) == lam x:A. f`x
  48.131  \subcaption{Functions and general product}
  48.132  \end{ttbox}
  48.133 -\caption{Further definitions of {\ZF}} \label{zf-defs}
  48.134 +\caption{Further definitions of ZF} \label{zf-defs}
  48.135  \end{figure}
  48.136  
  48.137  
  48.138 @@ -515,7 +513,7 @@
  48.139  \tdx{PowD}            A : Pow(B)  ==>  A<=B
  48.140  \subcaption{The empty set; power sets}
  48.141  \end{ttbox}
  48.142 -\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}
  48.143 +\caption{Basic derived rules for ZF} \label{zf-lemmas1}
  48.144  \end{figure}
  48.145  
  48.146  
  48.147 @@ -555,7 +553,7 @@
  48.148  Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
  48.149  The empty intersection should be undefined.  We cannot have
  48.150  $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set.  All
  48.151 -expressions denote something in {\ZF} set theory; the definition of
  48.152 +expressions denote something in ZF set theory; the definition of
  48.153  intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
  48.154  arbitrary.  The rule \tdx{InterI} must have a premise to exclude
  48.155  the empty intersection.  Some of the laws governing intersections require
  48.156 @@ -1051,7 +1049,7 @@
  48.157  See file \texttt{ZF/equalities.ML}.
  48.158  
  48.159  Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
  48.160 -operators including a conditional (Fig.\ts\ref{zf-bool}).  Although {\ZF} is a
  48.161 +operators including a conditional (Fig.\ts\ref{zf-bool}).  Although ZF is a
  48.162  first-order theory, you can obtain the effect of higher-order logic using
  48.163  \texttt{bool}-valued functions, for example.  The constant~\texttt{1} is
  48.164  translated to \texttt{succ(0)}.
  48.165 @@ -1343,13 +1341,13 @@
  48.166  
  48.167  \section{Automatic Tools}
  48.168  
  48.169 -{\ZF} provides the simplifier and the classical reasoner.   Moreover it
  48.170 -supplies a specialized tool to infer `types' of terms.
  48.171 +ZF provides the simplifier and the classical reasoner.  Moreover it supplies a
  48.172 +specialized tool to infer `types' of terms.
  48.173  
  48.174  \subsection{Simplification}
  48.175  
  48.176 -{\ZF} inherits simplification from {\FOL} but adopts it for set theory.  The
  48.177 -extraction of rewrite rules takes the {\ZF} primitives into account.  It can
  48.178 +ZF inherits simplification from FOL but adopts it for set theory.  The
  48.179 +extraction of rewrite rules takes the ZF primitives into account.  It can
  48.180  strip bounded universal quantifiers from a formula; for example, ${\forall
  48.181    x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp
  48.182  f(x)=g(x)$.  Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in
  48.183 @@ -1360,10 +1358,9 @@
  48.184  works for most purposes.  A small simplification set for set theory is
  48.185  called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal
  48.186  starting point.  \texttt{ZF_ss} contains congruence rules for all the binding
  48.187 -operators of {\ZF}\@.  It contains all the conversion rules, such as
  48.188 -\texttt{fst} and \texttt{snd}, as well as the rewrites shown in
  48.189 -Fig.\ts\ref{zf-simpdata}.  See the file \texttt{ZF/simpdata.ML} for a fuller
  48.190 -list.
  48.191 +operators of ZF.  It contains all the conversion rules, such as \texttt{fst}
  48.192 +and \texttt{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}.
  48.193 +See the file \texttt{ZF/simpdata.ML} for a fuller list.
  48.194  
  48.195  
  48.196  \subsection{Classical Reasoning}
  48.197 @@ -1396,7 +1393,7 @@
  48.198  \subsection{Type-Checking Tactics}
  48.199  \index{type-checking tactics}
  48.200  
  48.201 -Isabelle/{\ZF} provides simple tactics to help automate those proofs that are
  48.202 +Isabelle/ZF provides simple tactics to help automate those proofs that are
  48.203  essentially type-checking.  Such proofs are built by applying rules such as
  48.204  these:
  48.205  \begin{ttbox}
  48.206 @@ -1614,13 +1611,13 @@
  48.207  \label{sec:ZF:datatype}
  48.208  \index{*datatype|(}
  48.209  
  48.210 -The \ttindex{datatype} definition package of \ZF\ constructs inductive
  48.211 -datatypes similar to those of \ML.  It can also construct coinductive
  48.212 -datatypes (codatatypes), which are non-well-founded structures such as
  48.213 -streams.  It defines the set using a fixed-point construction and proves
  48.214 -induction rules, as well as theorems for recursion and case combinators.  It
  48.215 -supplies mechanisms for reasoning about freeness.  The datatype package can
  48.216 -handle both mutual and indirect recursion.
  48.217 +The \ttindex{datatype} definition package of ZF constructs inductive datatypes
  48.218 +similar to those of \ML.  It can also construct coinductive datatypes
  48.219 +(codatatypes), which are non-well-founded structures such as streams.  It
  48.220 +defines the set using a fixed-point construction and proves induction rules,
  48.221 +as well as theorems for recursion and case combinators.  It supplies
  48.222 +mechanisms for reasoning about freeness.  The datatype package can handle both
  48.223 +mutual and indirect recursion.
  48.224  
  48.225  
  48.226  \subsection{Basics}
  48.227 @@ -2440,10 +2437,10 @@
  48.228  proves the two equivalent.  It contains several datatype and inductive
  48.229  definitions, and demonstrates their use.
  48.230  
  48.231 -The directory \texttt{ZF/ex} contains further developments in {\ZF} set
  48.232 -theory.  Here is an overview; see the files themselves for more details.  I
  48.233 -describe much of this material in other
  48.234 -publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. 
  48.235 +The directory \texttt{ZF/ex} contains further developments in ZF set theory.
  48.236 +Here is an overview; see the files themselves for more details.  I describe
  48.237 +much of this material in other
  48.238 +publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.
  48.239  \begin{itemize}
  48.240  \item File \texttt{misc.ML} contains miscellaneous examples such as
  48.241    Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition
    49.1 --- a/doc-src/ZF/logics-ZF.tex	Mon Aug 28 13:50:24 2000 +0200
    49.2 +++ b/doc-src/ZF/logics-ZF.tex	Mon Aug 28 13:52:38 2000 +0200
    49.3 @@ -1,6 +1,6 @@
    49.4  %% $Id$
    49.5  \documentclass[11pt,a4paper]{report}
    49.6 -\usepackage{graphicx,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
    49.7 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
    49.8  
    49.9  %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
   49.10  %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
   49.11 @@ -15,8 +15,8 @@
   49.12          \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
   49.13          With Contributions by Tobias Nipkow and Markus Wenzel%
   49.14  \thanks{Markus Wenzel made numerous improvements.
   49.15 -    Philippe de Groote contributed to~\ZF{}.  Philippe No\"el and
   49.16 -    Martin Coen made many contributions to~\ZF{}.  The research has 
   49.17 +    Philippe de Groote contributed to~ZF.  Philippe No\"el and
   49.18 +    Martin Coen made many contributions to~ZF.  The research has 
   49.19      been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
   49.20      GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
   49.21      Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm