# HG changeset patch
# User wenzelm
# Date 909164120 -7200
# Node ID 369dca267a3b6f4ee15d37eebb05b142565f6853
# Parent  7ab9dd4a8ba6aa47394f7eafc076bbb31432bc07
SYNC: records (draft version);

diff -r 7ab9dd4a8ba6 -r 369dca267a3b doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Oct 23 18:51:54 1998 +0200
+++ b/doc-src/Logics/HOL.tex	Fri Oct 23 19:35:20 1998 +0200
@@ -1242,7 +1242,7 @@
 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
 the standard convention.
 \begin{ttbox}
-\sdx{primrec} "op +" nat 
+\sdx{primrec}
   "    0 + n = n"
   "Suc m + n = Suc(m + n)"
 \end{ttbox}
@@ -1539,17 +1539,80 @@
 class of all \HOL\ types.
 \end{warn}
 
-\section{Record types}
+
+\section{Records}
 
 At a first approximation, records are just a minor generalization of tuples,
 where components may be addressed by labels instead of just position.  The
 version of records offered by Isabelle/HOL is slightly more advanced, though,
-supporting \emph{extensible record schemes}.  This admits polymorphic
-operations wrt.\ record extensions, yielding ``object-oriented'' effects like
+supporting \emph{extensible record schemes}.  This admits operations that are
+polymorphic wrt.\ record extensions, yielding ``object-oriented'' effects like
 (single) inheritance.  See also \cite{Naraschewski-Wenzel:1998:TPHOL} for more
 details on object-oriented verification and record subtyping in HOL.
 
-\subsection{Defining records}
+\subsection{Basics}
+
+Isabelle/HOL supports concrete syntax for both fixed and schematic record
+terms and types:
+
+\begin{tabular}{l|l|l}
+  & terms & types \\ \hline
+  fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
+  scheme & $\record{x = a\fs y = b\fs \more = more}$ &
+    $\record{x \ty A\fs y \ty B\fs \more \ty \mu}$ \\
+\end{tabular}
+
+The \textsc{ascii} representation of $\record{~}$ is \texttt{(|~|)}.
+
+A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
+$y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,
+assuming $a \ty A$ and $b \ty B$.
+
+A record scheme like $\record{x = a\fs y = b\fs \more = more}$ contains fields
+$x$ and $y$ as before, but also possibly further fields as indicated by above
+``$\more$'' notation.  We call ``$\more$'' the \emph{more part}; logically it
+is just a free variable.  In the literature this is also referred to as
+\emph{row variable}.  The more part of record schemes may be instantiated by
+zero or more further components.  For example, above scheme might get
+instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = more'}$, where
+$more'$ refers to a different more part.
+
+Fixed records are special instances of record schemes, where $more$ is
+properly terminated by the $unit$ element $()$.  Thus $\record{x = a\fs y =
+  b}$ is just an abbreviation of $\record{x = a\fs y = b\fs \more = ()}$.
+
+\medskip
+
+There are two key features that make extensible records in a simply typed
+language like HOL feasible:
+\begin{enumerate}
+\item the ``more'' part is internalized (as a free term or type variable),
+\item field names are externalized, i.e.\ cannot be reasoned about within the
+  logic as first class values.
+\end{enumerate}
+
+\medskip
+
+Records have to be defined explicitly, fixing their field names and types,
+and (optional) parent record scheme (see \S\ref{sec:HOL:record-def}).
+Afterwards, records may be formed using above syntax, while obeying the
+canonical order of fields according to the declaration hierarchy.
+
+The record package also provides several operations like selectors and updates
+(see \S\ref{sec:HOL:record-ops}, together with their characteristics properties
+(see \S\ref{sec:HOL:record-thms}).
+
+There is a simple example exhibiting most basic aspects of extensible records
+available.  See theory \texttt{HOL/ex/Points} in the Isabelle sources.
+
+
+\subsection{Defining records}\label{sec:HOL:record-def}
+
+The theory syntax for record type definitions is shown in
+Fig.~\ref{fig:HOL:record}.  For the definition of `typevarlist' and `type' see
+\iflabelundefined{chap:classical}
+{the appendix of the {\em Reference Manual\/}}%
+{Appendix~\ref{app:TheorySyntax}}.
 
 \begin{figure}[htbp]
 \begin{rail}
@@ -1561,17 +1624,114 @@
 \label{fig:HOL:record}
 \end{figure}
 
-Records have to be defined explicitely, fixing their field names and types,
-and (optional) parent record scheme.  The theory syntax for record type
-definitions is shown in Fig.~\ref{fig:HOL:record}.  For the definition of
-`typevarlist' and `type' see \iflabelundefined{chap:classical}
-{the appendix of the {\em Reference Manual\/}}%
-{Appendix~\ref{app:TheorySyntax}}.
-
-
-\subsection{Record operations and syntax}
-
-\subsection{Proof tools}
+A general \ttindex{record} specification is of the following form:
+\[
+\mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
+  (\tau@1, \dots, \tau@m) \, s + c@1 :: \sigma@1 ~ \dots c@l :: \sigma@k
+\]
+where $\alpha@i$ are distinct type variables, and $\tau@i$, $\sigma@i$ types
+containing at most variables $\alpha@1, \dots, \alpha@n$; type constructor $t$
+has to be new, while $s$ specifies an existing one.  Also, the $c@i$ have to
+be distinct fields names (which may be safely reused from other records).
+Note that there has to be at least one field.
+
+\medskip
+
+Above definition introduces a new record type $(\alpha@1, \dots, \alpha@n) \,
+t$ by extending an existing one $(\tau@1, \dots, \tau@m) \, s$ by new fields
+$c@1, \dots, c@n$.  The parent record specification is optional.  By omitting
+it, $(\alpha@1, \dots, \alpha@n) \,t$ becomes a root record which is not
+derived from any other one.  The hierarchy of records declared within any
+theory forms a forest structure.
+
+The new type $(\alpha@1, \dots, \alpha@n) \, t$ is made an abbreviation for
+the fixed record type $\record{c@1 \ty \sigma@1\fs \dots\fs c@k \ty
+  \sigma@k}$, and $(\alpha@1\fs \dots\fs \alpha@n\fs \mu) \, t_scheme$ is made
+an abbreviation for $\record{c@1 \ty \sigma@1\fs \dots\fs c@k \ty \sigma@k\fs
+  \more \ty \mu}$.
+
+
+\subsection{Record operations}\label{sec:HOL:record-ops}
+
+Any record definition as above produces selectors, updates and derived
+constructors (make).  To simplify the presentation we assume that $(\alpha@1,
+\dots, \alpha@n) \, t$ is a root record with fields $c@i \ty \sigma@i$.
+
+Selectors and updates are available for any field proper field and the
+pseudo-field $more$ as follows:
+\begin{matharray}{lll}
+  c@i & \ty & (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \To \sigma@i \\
+  c@i_update & \ty & \sigma@i \To (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \To
+    (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \To
+\end{matharray}
+
+There is special syntax for updates: $r \, \record{x \asn a}$ abbreviates
+$x_update \, a \, r$.  Repeated updates are also supported like $r \,
+\record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
+$r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.  Note that because of
+postfix notation the order of fields printed is reverse in the actual term.
+This might be confusion under rare circumstances in conjunction with proof
+tools like ordered rewriting.
+
+Updates are just function applications, so fields may be freely permuted in
+the $\record{x \asn a\fs y \asn b}$ notation, as far as the logic is
+concerned.  Thus commutativity of updates can be proven within the logic for
+any two fields, not as a general theorem (remember that fields are not
+first-class).
+
+\medskip
+
+For convenience there are also derived record constructors as follows:
+\begin{matharray}{lll}
+  make & \ty & \sigma@1 \To \dots \To \sigma@k \To
+    (\alpha@1, \dots, \alpha@n) \, t \\
+  make_scheme & \ty & \sigma@1 \To \dots \To \sigma@k \To \mu \To
+    (\alpha@1, \dots, \alpha@n, \mu) \, t_scheme \\
+\end{matharray}
+
+\medskip
+
+Any of these operations are declared within a local name space for $t$.  In
+case that different records share field (base) names, one has to qualify
+explicitly, e.g.\ $t.c_update$.  This is recommended especially for generic
+names like $make$, which should be rather $t.make$ to avoid confusion.
+
+\medskip
+
+Reconsider the case of records that are derived of some parent record.  In
+general, the latter may depend on another parent as well, resulting in a list
+of ancestor records.  Appending the lists of fields of all ancestors results
+in a certain field prefix.  The Isabelle/HOL record package automatically
+takes care of this context of parent fields when defining selectors, updates
+etc.
+
+
+\subsection{Proof tools}\label{sec:HOL:record-thms}
+
+The record package provides the following proof rules for any record $t$:
+\begin{enumerate}
+
+\item standard conversions (selectors or updates applied to record constructor
+  terms) are part of the standard simpset,
+  
+\item inject equations of the form analogous to $((x, y) = (x', y')) \equiv
+  x=x' \conj y=y'$ are made part of standard simpset and claset (via
+  \texttt{addIffs}),
+  
+\item a tactic for record field splitting (\ttindex{record_split_tac}) is made
+  part of the standard claset (as sage wrapper); this is based on a rule like
+  this: $(\all x PROP~P~x) \equiv (\all{a~b} PROP~P(a, b))$.
+\end{enumerate}
+
+The first two kinds of rules are also stored within the theory as $t.simps$
+and $t.iffs$, respectively.
+
+The example \texttt{HOL/ex/Points} demonstrates typical proofs concerning
+records.  The basic idea is to make \ttindex{record_split_tac} expand
+quantified record variables and then simplify by the conversion rules.  By
+using a combination of the simplifier and classical prover together with the
+default simpset and claset, record problems should be solved (e.g.\ 
+\texttt{Auto_tac} or \texttt{Force_tac}) with a single stroke.
 
 
 \section{Datatype definitions}
@@ -2423,8 +2583,8 @@
 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
   distributed with Isabelle.}  %
 which you should refer to in case of difficulties.  The package is simpler
-than \ZF's thanks to \HOL's automatic type-checking.  The type of the
-(co)inductive determines the domain of the fixedpoint definition, and the
+than \ZF's thanks to \HOL's automatic type-checking.  The types of the
+(co)inductive sets determine the domain of the fixedpoint definition, and the
 package does not use inference rules for type-checking.
 
 
@@ -2446,7 +2606,7 @@
 \item[\tt elims] is the list of elimination rule.
 
 \item[\tt elim] is the head of the list {\tt elims}.
-
+  
 \item[\tt mk_cases] is a function to create simplified instances of {\tt
 elim}, using freeness reasoning on some underlying datatype.
 \end{description}
@@ -2513,11 +2673,7 @@
 \item The theory must separately declare the recursive sets as
   constants.
   
-\item The names of the recursive sets must be alphanumeric
-  identifiers.
-
-\item Side-conditions of the form $x=t$, where the variable~$x$ does not
-  occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
+\item The names of the recursive sets should be alphanumeric identifiers.
 \end{itemize}
 
 
diff -r 7ab9dd4a8ba6 -r 369dca267a3b doc-src/Logics/logics.ind
--- a/doc-src/Logics/logics.ind	Fri Oct 23 18:51:54 1998 +0200
+++ b/doc-src/Logics/logics.ind	Fri Oct 23 19:35:20 1998 +0200
@@ -3,64 +3,64 @@
   \item {\tt !} symbol, 60, 62, 69, 70, 82
   \item {\tt[]} symbol, 82
   \item {\tt\#} symbol, 82
-  \item {\tt\#*} symbol, 48, 133
-  \item {\tt\#+} symbol, 48, 133
+  \item {\tt\#*} symbol, 48, 136
+  \item {\tt\#+} symbol, 48, 136
   \item {\tt\#-} symbol, 48
-  \item {\tt\&} symbol, 7, 60, 110
-  \item {\tt *} symbol, 27, 61, 79, 124
+  \item {\tt\&} symbol, 7, 60, 113
+  \item {\tt *} symbol, 27, 61, 79, 127
   \item {\tt *} type, 77
-  \item {\tt +} symbol, 44, 61, 79, 124
+  \item {\tt +} symbol, 44, 61, 79, 127
   \item {\tt +} type, 77
-  \item {\tt -} symbol, 26, 61, 79, 133
-  \item {\tt -->} symbol, 7, 60, 110, 124
+  \item {\tt -} symbol, 26, 61, 79, 136
+  \item {\tt -->} symbol, 7, 60, 113, 127
   \item {\tt ->} symbol, 27
   \item {\tt -``} symbol, 26
   \item {\tt :} symbol, 26, 68
   \item {\tt <} constant, 80
   \item {\tt <} symbol, 79
-  \item {\tt <->} symbol, 7, 110
+  \item {\tt <->} symbol, 7, 113
   \item {\tt <=} constant, 80
   \item {\tt <=} symbol, 26, 68
-  \item {\tt =} symbol, 7, 60, 110, 124
+  \item {\tt =} symbol, 7, 60, 113, 127
   \item {\tt ?} symbol, 60, 62, 69, 70
   \item {\tt ?!} symbol, 60
   \item {\tt\at} symbol, 60, 82
-  \item {\tt `} symbol, 26, 124
+  \item {\tt `} symbol, 26, 127
   \item {\tt ``} symbol, 26, 68
   \item \verb'{}' symbol, 68
-  \item {\tt |} symbol, 7, 60, 110
-  \item {\tt |-|} symbol, 133
+  \item {\tt |} symbol, 7, 60, 113
+  \item {\tt |-|} symbol, 136
 
   \indexspace
 
-  \item {\tt 0} constant, 26, 79, 122
+  \item {\tt 0} constant, 26, 79, 125
 
   \indexspace
 
-  \item {\tt absdiff_def} theorem, 133
-  \item {\tt add_assoc} theorem, 133
-  \item {\tt add_commute} theorem, 133
-  \item {\tt add_def} theorem, 48, 133
-  \item {\tt add_inverse_diff} theorem, 133
-  \item {\tt add_mp_tac}, \bold{131}
-  \item {\tt add_mult_dist} theorem, 48, 133
-  \item {\tt add_safes}, \bold{116}
-  \item {\tt add_typing} theorem, 133
-  \item {\tt add_unsafes}, \bold{116}
-  \item {\tt addC0} theorem, 133
-  \item {\tt addC_succ} theorem, 133
+  \item {\tt absdiff_def} theorem, 136
+  \item {\tt add_assoc} theorem, 136
+  \item {\tt add_commute} theorem, 136
+  \item {\tt add_def} theorem, 48, 136
+  \item {\tt add_inverse_diff} theorem, 136
+  \item {\tt add_mp_tac}, \bold{134}
+  \item {\tt add_mult_dist} theorem, 48, 136
+  \item {\tt add_safes}, \bold{119}
+  \item {\tt add_typing} theorem, 136
+  \item {\tt add_unsafes}, \bold{119}
+  \item {\tt addC0} theorem, 136
+  \item {\tt addC_succ} theorem, 136
   \item {\tt Addsplits}, \bold{76}
-  \item {\tt addsplits}, \bold{76}, 81, 90
-  \item {\tt ALL} symbol, 7, 27, 60, 62, 69, 70, 110
-  \item {\tt All} constant, 7, 60, 110
+  \item {\tt addsplits}, \bold{76}, 81, 92
+  \item {\tt ALL} symbol, 7, 27, 60, 62, 69, 70, 113
+  \item {\tt All} constant, 7, 60, 113
   \item {\tt All_def} theorem, 64
   \item {\tt all_dupE} theorem, 5, 9, 66
   \item {\tt all_impE} theorem, 9
   \item {\tt allE} theorem, 5, 9, 66
   \item {\tt allI} theorem, 8, 66
-  \item {\tt allL} theorem, 112, 116
-  \item {\tt allL_thin} theorem, 113
-  \item {\tt allR} theorem, 112
+  \item {\tt allL} theorem, 115, 119
+  \item {\tt allL_thin} theorem, 116
+  \item {\tt allR} theorem, 115
   \item {\tt and_def} theorem, 43, 64
   \item {\tt app_def} theorem, 50
   \item {\tt apply_def} theorem, 32
@@ -70,10 +70,10 @@
   \item {\tt apply_Pair} theorem, 40, 58
   \item {\tt apply_type} theorem, 40
   \item {\tt arg_cong} theorem, 65
-  \item {\tt Arith} theory, 47, 80, 132
+  \item {\tt Arith} theory, 47, 80, 135
   \item assumptions
     \subitem contradictory, 16
-    \subitem in {\CTT}, 121, 131
+    \subitem in {\CTT}, 124, 134
 
   \indexspace
 
@@ -82,9 +82,9 @@
   \item {\tt Ball_def} theorem, 31, 71
   \item {\tt ballE} theorem, 33, 34, 72
   \item {\tt ballI} theorem, 34, 72
-  \item {\tt basic} theorem, 112
-  \item {\tt basic_defs}, \bold{129}
-  \item {\tt best_tac}, \bold{117}
+  \item {\tt basic} theorem, 115
+  \item {\tt basic_defs}, \bold{132}
+  \item {\tt best_tac}, \bold{120}
   \item {\tt beta} theorem, 40, 41
   \item {\tt Bex} constant, 26, 30, 68, 70
   \item {\tt bex_cong} theorem, 33, 34
@@ -112,7 +112,7 @@
   \indexspace
 
   \item {\tt case} constant, 44
-  \item {\tt case} symbol, 63, 80, 81, 90
+  \item {\tt case} symbol, 63, 80, 81, 92
   \item {\tt case_def} theorem, 44
   \item {\tt case_Inl} theorem, 44
   \item {\tt case_Inr} theorem, 44
@@ -121,23 +121,23 @@
   \item {\tt ccontr} theorem, 66
   \item {\tt classical} theorem, 66
   \item {\tt coinduct} theorem, 45
-  \item {\tt coinductive}, 102--105
+  \item {\tt coinductive}, 104--107
   \item {\tt Collect} constant, 26, 27, 30, 68, 70
   \item {\tt Collect_def} theorem, 31
   \item {\tt Collect_mem_eq} theorem, 70, 71
   \item {\tt Collect_subset} theorem, 37
-  \item {\tt CollectD} theorem, 72, 108
+  \item {\tt CollectD} theorem, 72, 110
   \item {\tt CollectD1} theorem, 33, 35
   \item {\tt CollectD2} theorem, 33, 35
   \item {\tt CollectE} theorem, 33, 35, 72
-  \item {\tt CollectI} theorem, 35, 72, 108
+  \item {\tt CollectI} theorem, 35, 72, 110
   \item {\tt comp_assoc} theorem, 46
   \item {\tt comp_bij} theorem, 46
   \item {\tt comp_def} theorem, 46
   \item {\tt comp_func} theorem, 46
   \item {\tt comp_func_apply} theorem, 46
   \item {\tt comp_inj} theorem, 46
-  \item {\tt comp_rls}, \bold{129}
+  \item {\tt comp_rls}, \bold{132}
   \item {\tt comp_surj} theorem, 46
   \item {\tt comp_type} theorem, 46
   \item {\tt Compl} constant, 68
@@ -158,12 +158,12 @@
   \item {\tt conj_impE} theorem, 9, 10
   \item {\tt conjE} theorem, 9, 65
   \item {\tt conjI} theorem, 8, 65
-  \item {\tt conjL} theorem, 112
-  \item {\tt conjR} theorem, 112
+  \item {\tt conjL} theorem, 115
+  \item {\tt conjR} theorem, 115
   \item {\tt conjunct1} theorem, 8, 65
   \item {\tt conjunct2} theorem, 8, 65
-  \item {\tt conL} theorem, 113
-  \item {\tt conR} theorem, 113
+  \item {\tt conL} theorem, 116
+  \item {\tt conR} theorem, 116
   \item {\tt cons} constant, 26, 27
   \item {\tt cons_def} theorem, 32
   \item {\tt Cons_iff} theorem, 50
@@ -172,38 +172,38 @@
   \item {\tt ConsI} theorem, 50
   \item {\tt consI1} theorem, 36
   \item {\tt consI2} theorem, 36
-  \item Constructive Type Theory, 121--143
-  \item {\tt contr} constant, 122
+  \item Constructive Type Theory, 124--146
+  \item {\tt contr} constant, 125
   \item {\tt converse} constant, 26, 40
   \item {\tt converse_def} theorem, 32
-  \item {\tt could_res}, \bold{115}
-  \item {\tt could_resolve_seq}, \bold{115}
-  \item {\tt CTT} theory, 1, 121
+  \item {\tt could_res}, \bold{118}
+  \item {\tt could_resolve_seq}, \bold{118}
+  \item {\tt CTT} theory, 1, 124
   \item {\tt Cube} theory, 1
-  \item {\tt cut} theorem, 112
+  \item {\tt cut} theorem, 115
   \item {\tt cut_facts_tac}, 19
-  \item {\tt cutL_tac}, \bold{114}
-  \item {\tt cutR_tac}, \bold{114}
+  \item {\tt cutL_tac}, \bold{117}
+  \item {\tt cutR_tac}, \bold{117}
 
   \indexspace
 
-  \item {\tt datatype}, 87--95
+  \item {\tt datatype}, 89--97
   \item {\tt Delsplits}, \bold{76}
   \item {\tt delsplits}, \bold{76}
-  \item {\tt diff_0_eq_0} theorem, 133
+  \item {\tt diff_0_eq_0} theorem, 136
   \item {\tt Diff_cancel} theorem, 42
   \item {\tt Diff_contains} theorem, 37
   \item {\tt Diff_def} theorem, 31
-  \item {\tt diff_def} theorem, 48, 133
+  \item {\tt diff_def} theorem, 48, 136
   \item {\tt Diff_disjoint} theorem, 42
   \item {\tt Diff_Int} theorem, 42
   \item {\tt Diff_partition} theorem, 42
-  \item {\tt diff_self_eq_0} theorem, 133
+  \item {\tt diff_self_eq_0} theorem, 136
   \item {\tt Diff_subset} theorem, 37
-  \item {\tt diff_succ_succ} theorem, 133
-  \item {\tt diff_typing} theorem, 133
+  \item {\tt diff_succ_succ} theorem, 136
+  \item {\tt diff_typing} theorem, 136
   \item {\tt Diff_Un} theorem, 42
-  \item {\tt diffC0} theorem, 133
+  \item {\tt diffC0} theorem, 136
   \item {\tt DiffD1} theorem, 36
   \item {\tt DiffD2} theorem, 36
   \item {\tt DiffE} theorem, 36
@@ -213,10 +213,10 @@
   \item {\tt disjE} theorem, 8, 65
   \item {\tt disjI1} theorem, 8, 65
   \item {\tt disjI2} theorem, 8, 65
-  \item {\tt disjL} theorem, 112
-  \item {\tt disjR} theorem, 112
-  \item {\tt div} symbol, 48, 79, 133
-  \item {\tt div_def} theorem, 48, 133
+  \item {\tt disjL} theorem, 115
+  \item {\tt disjR} theorem, 115
+  \item {\tt div} symbol, 48, 79, 136
+  \item {\tt div_def} theorem, 48, 136
   \item {\tt div_geq} theorem, 80
   \item {\tt div_less} theorem, 80
   \item {\tt Divides} theory, 80
@@ -234,28 +234,28 @@
 
   \indexspace
 
-  \item {\tt Elem} constant, 122
-  \item {\tt elim_rls}, \bold{129}
-  \item {\tt elimL_rls}, \bold{129}
+  \item {\tt Elem} constant, 125
+  \item {\tt elim_rls}, \bold{132}
+  \item {\tt elimL_rls}, \bold{132}
   \item {\tt empty_def} theorem, 71
-  \item {\tt empty_pack}, \bold{115}
+  \item {\tt empty_pack}, \bold{118}
   \item {\tt empty_subsetI} theorem, 34
   \item {\tt emptyE} theorem, 34, 73
   \item {\tt Eps} constant, 60, 62
-  \item {\tt Eq} constant, 122
-  \item {\tt eq} constant, 122, 127
+  \item {\tt Eq} constant, 125
+  \item {\tt eq} constant, 125, 130
   \item {\tt eq_mp_tac}, \bold{10}
-  \item {\tt EqC} theorem, 128
-  \item {\tt EqE} theorem, 128
-  \item {\tt Eqelem} constant, 122
-  \item {\tt EqF} theorem, 128
-  \item {\tt EqFL} theorem, 128
-  \item {\tt EqI} theorem, 128
-  \item {\tt Eqtype} constant, 122
-  \item {\tt equal_tac}, \bold{130}
-  \item {\tt equal_types} theorem, 125
-  \item {\tt equal_typesL} theorem, 125
-  \item {\tt equalityCE} theorem, 70, 72, 107, 108
+  \item {\tt EqC} theorem, 131
+  \item {\tt EqE} theorem, 131
+  \item {\tt Eqelem} constant, 125
+  \item {\tt EqF} theorem, 131
+  \item {\tt EqFL} theorem, 131
+  \item {\tt EqI} theorem, 131
+  \item {\tt Eqtype} constant, 125
+  \item {\tt equal_tac}, \bold{133}
+  \item {\tt equal_types} theorem, 128
+  \item {\tt equal_typesL} theorem, 128
+  \item {\tt equalityCE} theorem, 70, 72, 110, 111
   \item {\tt equalityD1} theorem, 34, 72
   \item {\tt equalityD2} theorem, 34, 72
   \item {\tt equalityE} theorem, 34, 72
@@ -264,8 +264,8 @@
   \item {\tt equals0I} theorem, 34
   \item {\tt eresolve_tac}, 16
   \item {\tt eta} theorem, 40, 41
-  \item {\tt EX} symbol, 7, 27, 60, 62, 69, 70, 110
-  \item {\tt Ex} constant, 7, 60, 110
+  \item {\tt EX} symbol, 7, 27, 60, 62, 69, 70, 113
+  \item {\tt Ex} constant, 7, 60, 113
   \item {\tt EX!} symbol, 7, 60
   \item {\tt Ex1} constant, 7, 60
   \item {\tt Ex1_def} theorem, 64
@@ -277,26 +277,26 @@
   \item {\tt exCI} theorem, 11, 15, 66
   \item {\tt excluded_middle} theorem, 11, 66
   \item {\tt exE} theorem, 8, 66
-  \item {\tt exhaust_tac}, \bold{92}
+  \item {\tt exhaust_tac}, \bold{93}
   \item {\tt exI} theorem, 8, 66
-  \item {\tt exL} theorem, 112
-  \item {\tt Exp} theory, 106
-  \item {\tt exR} theorem, 112, 116, 117
-  \item {\tt exR_thin} theorem, 113, 117, 118
+  \item {\tt exL} theorem, 115
+  \item {\tt Exp} theory, 108
+  \item {\tt exR} theorem, 115, 119, 120
+  \item {\tt exR_thin} theorem, 116, 120, 121
   \item {\tt ext} theorem, 63, 64
   \item {\tt extension} theorem, 31
 
   \indexspace
 
-  \item {\tt F} constant, 122
-  \item {\tt False} constant, 7, 60, 110
+  \item {\tt F} constant, 125
+  \item {\tt False} constant, 7, 60, 113
   \item {\tt False_def} theorem, 64
   \item {\tt FalseE} theorem, 8, 65
-  \item {\tt FalseL} theorem, 112
-  \item {\tt fast_tac}, \bold{117}
-  \item {\tt FE} theorem, 128, 132
-  \item {\tt FEL} theorem, 128
-  \item {\tt FF} theorem, 128
+  \item {\tt FalseL} theorem, 115
+  \item {\tt fast_tac}, \bold{120}
+  \item {\tt FE} theorem, 131, 135
+  \item {\tt FEL} theorem, 131
+  \item {\tt FF} theorem, 131
   \item {\tt field} constant, 26
   \item {\tt field_def} theorem, 32
   \item {\tt field_subset} theorem, 39
@@ -304,8 +304,8 @@
   \item {\tt fieldE} theorem, 39
   \item {\tt fieldI1} theorem, 39
   \item {\tt fieldI2} theorem, 39
-  \item {\tt filseq_resolve_tac}, \bold{115}
-  \item {\tt filt_resolve_tac}, 115, 130
+  \item {\tt filseq_resolve_tac}, \bold{118}
+  \item {\tt filt_resolve_tac}, 118, 133
   \item {\tt filter} constant, 82
   \item {\tt Fin.consI} theorem, 49
   \item {\tt Fin.emptyI} theorem, 49
@@ -318,18 +318,18 @@
   \item {\tt Fixedpt} theory, 43
   \item {\tt flat} constant, 50
   \item {\tt flat_def} theorem, 50
-  \item flex-flex constraints, 111
-  \item {\tt FOL} theory, 1, 5, 11, 131
+  \item flex-flex constraints, 114
+  \item {\tt FOL} theory, 1, 5, 11, 134
   \item {\tt FOL_cs}, \bold{11}
   \item {\tt FOL_ss}, \bold{6}
   \item {\tt foldl} constant, 82
-  \item {\tt form_rls}, \bold{129}
-  \item {\tt formL_rls}, \bold{129}
-  \item {\tt forms_of_seq}, \bold{114}
+  \item {\tt form_rls}, \bold{132}
+  \item {\tt formL_rls}, \bold{132}
+  \item {\tt forms_of_seq}, \bold{117}
   \item {\tt foundation} theorem, 31
-  \item {\tt fst} constant, 26, 33, 77, 122, 127
+  \item {\tt fst} constant, 26, 33, 77, 125, 130
   \item {\tt fst_conv} theorem, 38, 77
-  \item {\tt fst_def} theorem, 32, 127
+  \item {\tt fst_def} theorem, 32, 130
   \item {\tt Fun} theory, 75
   \item {\textit {fun}} type, 61
   \item {\tt fun_cong} theorem, 65
@@ -341,7 +341,7 @@
   \item {\tt fun_is_rel} theorem, 40
   \item {\tt fun_single} theorem, 41
   \item function applications
-    \subitem in \CTT, 124
+    \subitem in \CTT, 127
     \subitem in \ZF, 26
 
   \indexspace
@@ -356,8 +356,8 @@
 
   \indexspace
 
-  \item {\tt hd} constant, 82, 99
-  \item higher-order logic, 59--108
+  \item {\tt hd} constant, 82, 102
+  \item higher-order logic, 59--111
   \item {\tt HOL} theory, 1, 59
   \item {\sc hol} system, 59, 62
   \item {\tt HOL_basic_ss}, \bold{75}
@@ -365,12 +365,12 @@
   \item {\tt HOL_quantifiers}, \bold{62}, 70
   \item {\tt HOL_ss}, \bold{75}
   \item {\tt HOLCF} theory, 1
-  \item {\tt hyp_rew_tac}, \bold{131}
+  \item {\tt hyp_rew_tac}, \bold{134}
   \item {\tt hyp_subst_tac}, 6, 75
 
   \indexspace
 
-  \item {\textit {i}} type, 25, 121
+  \item {\textit {i}} type, 25, 124
   \item {\tt id} constant, 46
   \item {\tt id_def} theorem, 46
   \item {\tt If} constant, 60
@@ -380,15 +380,15 @@
   \item {\tt if_P} theorem, 36, 66
   \item {\tt ifE} theorem, 19
   \item {\tt iff} theorem, 63, 64
-  \item {\tt iff_def} theorem, 8, 112
+  \item {\tt iff_def} theorem, 8, 115
   \item {\tt iff_impE} theorem, 9
   \item {\tt iffCE} theorem, 11, 66, 70
   \item {\tt iffD1} theorem, 9, 65
   \item {\tt iffD2} theorem, 9, 65
   \item {\tt iffE} theorem, 9, 65
   \item {\tt iffI} theorem, 9, 19, 65
-  \item {\tt iffL} theorem, 113, 119
-  \item {\tt iffR} theorem, 113
+  \item {\tt iffL} theorem, 116, 122
+  \item {\tt iffR} theorem, 116
   \item {\tt ifI} theorem, 19
   \item {\tt IFOL} theory, 5
   \item {\tt IFOL_ss}, \bold{6}
@@ -399,13 +399,13 @@
   \item {\tt impCE} theorem, 11, 66
   \item {\tt impE} theorem, 9, 10, 65
   \item {\tt impI} theorem, 8, 63
-  \item {\tt impL} theorem, 112
-  \item {\tt impR} theorem, 112
+  \item {\tt impL} theorem, 115
+  \item {\tt impR} theorem, 115
   \item {\tt in} symbol, 28, 61
   \item {\textit {ind}} type, 78
   \item {\tt induct} theorem, 45
-  \item {\tt induct_tac}, 80, \bold{92}
-  \item {\tt inductive}, 102--105
+  \item {\tt induct_tac}, 80, \bold{93}
+  \item {\tt inductive}, 104--107
   \item {\tt Inf} constant, 26, 30
   \item {\tt infinity} theorem, 32
   \item {\tt inj} constant, 46, 75
@@ -417,13 +417,13 @@
   \item {\tt inj_on_def} theorem, 75
   \item {\tt inj_Suc} theorem, 79
   \item {\tt Inl} constant, 44, 79
-  \item {\tt inl} constant, 122, 127, 137
+  \item {\tt inl} constant, 125, 130, 140
   \item {\tt Inl_def} theorem, 44
   \item {\tt Inl_inject} theorem, 44
   \item {\tt Inl_neq_Inr} theorem, 44
   \item {\tt Inl_not_Inr} theorem, 79
   \item {\tt Inr} constant, 44, 79
-  \item {\tt inr} constant, 122, 127
+  \item {\tt inr} constant, 125, 130
   \item {\tt Inr_def} theorem, 44
   \item {\tt Inr_inject} theorem, 44
   \item {\tt insert} constant, 68
@@ -469,21 +469,21 @@
   \item {\tt IntPr.safe_step_tac}, \bold{10}
   \item {\tt IntPr.safe_tac}, \bold{10}
   \item {\tt IntPr.step_tac}, \bold{10}
-  \item {\tt intr_rls}, \bold{129}
-  \item {\tt intr_tac}, \bold{130}, 139, 140
-  \item {\tt intrL_rls}, \bold{129}
+  \item {\tt intr_rls}, \bold{132}
+  \item {\tt intr_tac}, \bold{133}, 142, 143
+  \item {\tt intrL_rls}, \bold{132}
   \item {\tt inv} constant, 75
   \item {\tt inv_def} theorem, 75
 
   \indexspace
 
-  \item {\tt lam} symbol, 27, 29, 124
+  \item {\tt lam} symbol, 27, 29, 127
   \item {\tt lam_def} theorem, 32
   \item {\tt lam_type} theorem, 40
   \item {\tt Lambda} constant, 26, 30
-  \item {\tt lambda} constant, 122, 124
+  \item {\tt lambda} constant, 125, 127
   \item $\lambda$-abstractions
-    \subitem in \CTT, 124
+    \subitem in \CTT, 127
     \subitem in \ZF, 27
   \item {\tt lamE} theorem, 40, 41
   \item {\tt lamI} theorem, 40, 41
@@ -502,7 +502,7 @@
   \item {\tt Let} constant, 25, 26, 60, 63
   \item {\tt let} symbol, 28, 61, 63
   \item {\tt Let_def} theorem, 25, 31, 63, 64
-  \item {\tt LFilter} theory, 106
+  \item {\tt LFilter} theory, 108
   \item {\tt lfp_def} theorem, 45
   \item {\tt lfp_greatest} theorem, 45
   \item {\tt lfp_lowerbound} theorem, 45
@@ -519,10 +519,10 @@
   \item {\tt list_rec_Cons} theorem, 50
   \item {\tt list_rec_def} theorem, 50
   \item {\tt list_rec_Nil} theorem, 50
-  \item {\tt LK} theory, 1, 109, 113
-  \item {\tt LK_dup_pack}, \bold{116}, 117
-  \item {\tt LK_pack}, \bold{116}
-  \item {\tt LList} theory, 106
+  \item {\tt LK} theory, 1, 112, 116
+  \item {\tt LK_dup_pack}, \bold{119}, 120
+  \item {\tt LK_pack}, \bold{119}
+  \item {\tt LList} theory, 108
   \item {\tt logic} class, 5
 
   \indexspace
@@ -541,29 +541,29 @@
   \item {\tt mem_irrefl} theorem, 36
   \item {\tt min} constant, 61, 80
   \item {\tt minus} class, 61
-  \item {\tt mod} symbol, 48, 79, 133
-  \item {\tt mod_def} theorem, 48, 133
+  \item {\tt mod} symbol, 48, 79, 136
+  \item {\tt mod_def} theorem, 48, 136
   \item {\tt mod_geq} theorem, 80
   \item {\tt mod_less} theorem, 80
   \item {\tt mod_quo_equality} theorem, 48
   \item {\tt Modal} theory, 1
   \item {\tt mono} constant, 61
   \item {\tt mp} theorem, 8, 63
-  \item {\tt mp_tac}, \bold{10}, \bold{131}
+  \item {\tt mp_tac}, \bold{10}, \bold{134}
   \item {\tt mult_0} theorem, 48
-  \item {\tt mult_assoc} theorem, 48, 133
-  \item {\tt mult_commute} theorem, 48, 133
-  \item {\tt mult_def} theorem, 48, 133
+  \item {\tt mult_assoc} theorem, 48, 136
+  \item {\tt mult_commute} theorem, 48, 136
+  \item {\tt mult_def} theorem, 48, 136
   \item {\tt mult_succ} theorem, 48
   \item {\tt mult_type} theorem, 48
-  \item {\tt mult_typing} theorem, 133
-  \item {\tt multC0} theorem, 133
-  \item {\tt multC_succ} theorem, 133
-  \item {\tt mutual_induct_tac}, \bold{92}
+  \item {\tt mult_typing} theorem, 136
+  \item {\tt multC0} theorem, 136
+  \item {\tt multC_succ} theorem, 136
+  \item {\tt mutual_induct_tac}, \bold{93}
 
   \indexspace
 
-  \item {\tt N} constant, 122
+  \item {\tt N} constant, 125
   \item {\tt n_not_Suc_n} theorem, 79
   \item {\tt Nat} theory, 47, 80
   \item {\textit {nat}} type, 79, 80
@@ -579,32 +579,32 @@
   \item {\tt nat_rec} constant, 80
   \item {\tt nat_succI} theorem, 48
   \item {\tt NatDef} theory, 78
-  \item {\tt NC0} theorem, 126
-  \item {\tt NC_succ} theorem, 126
-  \item {\tt NE} theorem, 125, 126, 134
-  \item {\tt NEL} theorem, 126
-  \item {\tt NF} theorem, 126, 135
-  \item {\tt NI0} theorem, 126
-  \item {\tt NI_succ} theorem, 126
-  \item {\tt NI_succL} theorem, 126
+  \item {\tt NC0} theorem, 129
+  \item {\tt NC_succ} theorem, 129
+  \item {\tt NE} theorem, 128, 129, 137
+  \item {\tt NEL} theorem, 129
+  \item {\tt NF} theorem, 129, 138
+  \item {\tt NI0} theorem, 129
+  \item {\tt NI_succ} theorem, 129
+  \item {\tt NI_succL} theorem, 129
   \item {\tt Nil_Cons_iff} theorem, 50
   \item {\tt NilI} theorem, 50
-  \item {\tt NIO} theorem, 134
-  \item {\tt Not} constant, 7, 60, 110
+  \item {\tt NIO} theorem, 137
+  \item {\tt Not} constant, 7, 60, 113
   \item {\tt not_def} theorem, 8, 43, 64
   \item {\tt not_impE} theorem, 9
   \item {\tt not_sym} theorem, 65
   \item {\tt notE} theorem, 9, 10, 65
   \item {\tt notI} theorem, 9, 65
-  \item {\tt notL} theorem, 112
+  \item {\tt notL} theorem, 115
   \item {\tt notnotD} theorem, 11, 66
-  \item {\tt notR} theorem, 112
+  \item {\tt notR} theorem, 115
   \item {\tt null} constant, 82
 
   \indexspace
 
   \item {\tt O} symbol, 46
-  \item {\textit {o}} type, 5, 109
+  \item {\textit {o}} type, 5, 112
   \item {\tt o} symbol, 60, 71
   \item {\tt o_def} theorem, 64
   \item {\tt of} symbol, 63
@@ -615,9 +615,9 @@
 
   \indexspace
 
-  \item {\tt pack} ML type, 115
+  \item {\tt pack} ML type, 118
   \item {\tt Pair} constant, 26, 27, 77
-  \item {\tt pair} constant, 122
+  \item {\tt pair} constant, 125
   \item {\tt Pair_def} theorem, 32
   \item {\tt Pair_eq} theorem, 77
   \item {\tt Pair_inject} theorem, 38, 77
@@ -626,52 +626,52 @@
   \item {\tt Pair_neq_0} theorem, 38
   \item {\tt PairE} theorem, 77
   \item {\tt pairing} theorem, 35
-  \item {\tt pc_tac}, \bold{117}, \bold{132}, 138, 139
+  \item {\tt pc_tac}, \bold{120}, \bold{135}, 141, 142
   \item {\tt Perm} theory, 43
   \item {\tt Pi} constant, 26, 29, 41
   \item {\tt Pi_def} theorem, 32
   \item {\tt Pi_type} theorem, 40, 41
   \item {\tt plus} class, 61
-  \item {\tt PlusC_inl} theorem, 128
-  \item {\tt PlusC_inr} theorem, 128
-  \item {\tt PlusE} theorem, 128, 132, 136
-  \item {\tt PlusEL} theorem, 128
-  \item {\tt PlusF} theorem, 128
-  \item {\tt PlusFL} theorem, 128
-  \item {\tt PlusI_inl} theorem, 128, 137
-  \item {\tt PlusI_inlL} theorem, 128
-  \item {\tt PlusI_inr} theorem, 128
-  \item {\tt PlusI_inrL} theorem, 128
+  \item {\tt PlusC_inl} theorem, 131
+  \item {\tt PlusC_inr} theorem, 131
+  \item {\tt PlusE} theorem, 131, 135, 139
+  \item {\tt PlusEL} theorem, 131
+  \item {\tt PlusF} theorem, 131
+  \item {\tt PlusFL} theorem, 131
+  \item {\tt PlusI_inl} theorem, 131, 140
+  \item {\tt PlusI_inlL} theorem, 131
+  \item {\tt PlusI_inr} theorem, 131
+  \item {\tt PlusI_inrL} theorem, 131
   \item {\tt Pow} constant, 26, 68
   \item {\tt Pow_def} theorem, 71
   \item {\tt Pow_iff} theorem, 31
   \item {\tt Pow_mono} theorem, 53
   \item {\tt PowD} theorem, 34, 54, 73
   \item {\tt PowI} theorem, 34, 54, 73
-  \item {\tt primrec}, 95--99
+  \item {\tt primrec}, 98--101
   \item {\tt primrec} symbol, 80
   \item {\tt PrimReplace} constant, 26, 30
   \item priorities, 2
-  \item {\tt PROD} symbol, 27, 29, 123, 124
-  \item {\tt Prod} constant, 122
+  \item {\tt PROD} symbol, 27, 29, 126, 127
+  \item {\tt Prod} constant, 125
   \item {\tt Prod} theory, 77
-  \item {\tt ProdC} theorem, 126, 142
-  \item {\tt ProdC2} theorem, 126
-  \item {\tt ProdE} theorem, 126, 139, 141, 143
-  \item {\tt ProdEL} theorem, 126
-  \item {\tt ProdF} theorem, 126
-  \item {\tt ProdFL} theorem, 126
-  \item {\tt ProdI} theorem, 126, 132, 134
-  \item {\tt ProdIL} theorem, 126
+  \item {\tt ProdC} theorem, 129, 145
+  \item {\tt ProdC2} theorem, 129
+  \item {\tt ProdE} theorem, 129, 142, 144, 146
+  \item {\tt ProdEL} theorem, 129
+  \item {\tt ProdF} theorem, 129
+  \item {\tt ProdFL} theorem, 129
+  \item {\tt ProdI} theorem, 129, 135, 137
+  \item {\tt ProdIL} theorem, 129
   \item {\tt prop_cs}, \bold{11}, \bold{76}
-  \item {\tt prop_pack}, \bold{115}
+  \item {\tt prop_pack}, \bold{118}
 
   \indexspace
 
   \item {\tt qcase_def} theorem, 44
   \item {\tt qconverse} constant, 43
   \item {\tt qconverse_def} theorem, 44
-  \item {\tt qed_spec_mp}, 93
+  \item {\tt qed_spec_mp}, 96
   \item {\tt qfsplit_def} theorem, 44
   \item {\tt QInl_def} theorem, 44
   \item {\tt QInr_def} theorem, 44
@@ -686,43 +686,45 @@
 
   \indexspace
 
-  \item {\tt range} constant, 26, 68, 107
+  \item {\tt range} constant, 26, 68, 109
   \item {\tt range_def} theorem, 32, 71
   \item {\tt range_of_fun} theorem, 40, 41
   \item {\tt range_subset} theorem, 39
   \item {\tt range_type} theorem, 40
-  \item {\tt rangeE} theorem, 39, 73, 107
+  \item {\tt rangeE} theorem, 39, 73, 110
   \item {\tt rangeI} theorem, 39, 73
   \item {\tt rank} constant, 49
   \item {\tt rank_ss}, \bold{24}
-  \item {\tt rec} constant, 48, 122, 125
+  \item {\tt rec} constant, 48, 125, 128
   \item {\tt rec_0} theorem, 48
   \item {\tt rec_def} theorem, 48
   \item {\tt rec_succ} theorem, 48
-  \item {\tt recdef}, 99--102
+  \item {\tt recdef}, 101--104
+  \item {\tt record}, 87
+  \item {\tt record_split_tac}, 89
   \item recursion
-    \subitem general, 99--102
-    \subitem primitive, 95--99
-  \item recursive functions, \see{recursion}{95}
-  \item {\tt red_if_equal} theorem, 125
-  \item {\tt Reduce} constant, 122, 125, 131
-  \item {\tt refl} theorem, 8, 63, 112
-  \item {\tt refl_elem} theorem, 125, 129
-  \item {\tt refl_red} theorem, 125
-  \item {\tt refl_type} theorem, 125, 129
-  \item {\tt REPEAT_FIRST}, 130
-  \item {\tt repeat_goal_tac}, \bold{117}
+    \subitem general, 101--104
+    \subitem primitive, 98--101
+  \item recursive functions, \see{recursion}{97}
+  \item {\tt red_if_equal} theorem, 128
+  \item {\tt Reduce} constant, 125, 128, 134
+  \item {\tt refl} theorem, 8, 63, 115
+  \item {\tt refl_elem} theorem, 128, 132
+  \item {\tt refl_red} theorem, 128
+  \item {\tt refl_type} theorem, 128, 132
+  \item {\tt REPEAT_FIRST}, 133
+  \item {\tt repeat_goal_tac}, \bold{120}
   \item {\tt RepFun} constant, 26, 29, 30, 33
   \item {\tt RepFun_def} theorem, 31
   \item {\tt RepFunE} theorem, 35
   \item {\tt RepFunI} theorem, 35
   \item {\tt Replace} constant, 26, 29, 30, 33
   \item {\tt Replace_def} theorem, 31
-  \item {\tt replace_type} theorem, 129, 141
+  \item {\tt replace_type} theorem, 132, 144
   \item {\tt ReplaceE} theorem, 35
   \item {\tt ReplaceI} theorem, 35
   \item {\tt replacement} theorem, 31
-  \item {\tt reresolve_tac}, \bold{117}
+  \item {\tt reresolve_tac}, \bold{120}
   \item {\tt res_inst_tac}, 62
   \item {\tt restrict} constant, 26, 33
   \item {\tt restrict} theorem, 40
@@ -731,31 +733,31 @@
   \item {\tt restrict_type} theorem, 40
   \item {\tt rev} constant, 50, 82
   \item {\tt rev_def} theorem, 50
-  \item {\tt rew_tac}, 19, \bold{131}
+  \item {\tt rew_tac}, 19, \bold{134}
   \item {\tt rewrite_rule}, 19
   \item {\tt right_comp_id} theorem, 46
   \item {\tt right_comp_inverse} theorem, 46
   \item {\tt right_inverse} theorem, 46
-  \item {\tt RL}, 136
-  \item {\tt RS}, 141, 143
+  \item {\tt RL}, 139
+  \item {\tt RS}, 144, 146
 
   \indexspace
 
-  \item {\tt safe_goal_tac}, \bold{117}
-  \item {\tt safe_tac}, \bold{132}
-  \item {\tt safestep_tac}, \bold{132}
+  \item {\tt safe_goal_tac}, \bold{120}
+  \item {\tt safe_tac}, \bold{135}
+  \item {\tt safestep_tac}, \bold{135}
   \item search
-    \subitem best-first, 108
+    \subitem best-first, 111
   \item {\tt select_equality} theorem, 64, 66
   \item {\tt selectI} theorem, 63, 64
   \item {\tt separation} theorem, 35
-  \item {\tt Seqof} constant, 110
-  \item sequent calculus, 109--120
+  \item {\tt Seqof} constant, 113
+  \item sequent calculus, 112--123
   \item {\tt Set} theory, 67, 70
   \item {\tt set} constant, 82
   \item {\tt set} type, 67
   \item set theory, 24--58
-  \item {\tt set_current_thy}, 108
+  \item {\tt set_current_thy}, 111
   \item {\tt set_diff_def} theorem, 71
   \item {\tt show_sorts}, 62
   \item {\tt show_types}, 62
@@ -768,13 +770,13 @@
     \subitem of conjunctions, 6, 75
   \item {\tt singletonE} theorem, 36
   \item {\tt singletonI} theorem, 36
-  \item {\tt size} constant, 90
-  \item {\tt snd} constant, 26, 33, 77, 122, 127
+  \item {\tt size} constant, 93
+  \item {\tt snd} constant, 26, 33, 77, 125, 130
   \item {\tt snd_conv} theorem, 38, 77
-  \item {\tt snd_def} theorem, 32, 127
-  \item {\tt sobj} type, 113
+  \item {\tt snd_def} theorem, 32, 130
+  \item {\tt sobj} type, 116
   \item {\tt spec} theorem, 8, 66
-  \item {\tt split} constant, 26, 33, 77, 122, 136
+  \item {\tt split} constant, 26, 33, 77, 125, 139
   \item {\tt split} theorem, 38, 77
   \item {\tt split_all_tac}, \bold{78}
   \item {\tt split_def} theorem, 32
@@ -785,7 +787,7 @@
   \item {\tt ssubst} theorem, 9, 65, 67
   \item {\tt stac}, \bold{75}
   \item {\tt Step_tac}, 22
-  \item {\tt step_tac}, 23, \bold{117}, \bold{132}
+  \item {\tt step_tac}, 23, \bold{120}, \bold{135}
   \item {\tt strip_tac}, \bold{67}
   \item {\tt subset_def} theorem, 31, 71
   \item {\tt subset_refl} theorem, 34, 72
@@ -794,15 +796,15 @@
   \item {\tt subsetD} theorem, 34, 56, 70, 72
   \item {\tt subsetI} theorem, 34, 54, 55, 72
   \item {\tt subst} theorem, 8, 63
-  \item {\tt subst_elem} theorem, 125
-  \item {\tt subst_elemL} theorem, 125
-  \item {\tt subst_eqtyparg} theorem, 129, 141
-  \item {\tt subst_prodE} theorem, 127, 129
-  \item {\tt subst_type} theorem, 125
-  \item {\tt subst_typeL} theorem, 125
+  \item {\tt subst_elem} theorem, 128
+  \item {\tt subst_elemL} theorem, 128
+  \item {\tt subst_eqtyparg} theorem, 132, 144
+  \item {\tt subst_prodE} theorem, 130, 132
+  \item {\tt subst_type} theorem, 128
+  \item {\tt subst_typeL} theorem, 128
   \item {\tt Suc} constant, 79
   \item {\tt Suc_not_Zero} theorem, 79
-  \item {\tt succ} constant, 26, 30, 122
+  \item {\tt succ} constant, 26, 30, 125
   \item {\tt succ_def} theorem, 32
   \item {\tt succ_inject} theorem, 36
   \item {\tt succ_neq_0} theorem, 36
@@ -810,8 +812,8 @@
   \item {\tt succE} theorem, 36
   \item {\tt succI1} theorem, 36
   \item {\tt succI2} theorem, 36
-  \item {\tt SUM} symbol, 27, 29, 123, 124
-  \item {\tt Sum} constant, 122
+  \item {\tt SUM} symbol, 27, 29, 126, 127
+  \item {\tt Sum} constant, 125
   \item {\tt Sum} theory, 43, 78
   \item {\tt sum_case} constant, 79
   \item {\tt sum_case_Inl} theorem, 79
@@ -823,69 +825,69 @@
   \item {\tt SUM_Int_distrib2} theorem, 42
   \item {\tt SUM_Un_distrib1} theorem, 42
   \item {\tt SUM_Un_distrib2} theorem, 42
-  \item {\tt SumC} theorem, 127
-  \item {\tt SumE} theorem, 127, 132, 136
+  \item {\tt SumC} theorem, 130
+  \item {\tt SumE} theorem, 130, 135, 139
   \item {\tt sumE} theorem, 79
   \item {\tt sumE2} theorem, 44
-  \item {\tt SumE_fst} theorem, 127, 129, 141, 142
-  \item {\tt SumE_snd} theorem, 127, 129, 143
-  \item {\tt SumEL} theorem, 127
-  \item {\tt SumF} theorem, 127
-  \item {\tt SumFL} theorem, 127
-  \item {\tt SumI} theorem, 127, 137
-  \item {\tt SumIL} theorem, 127
-  \item {\tt SumIL2} theorem, 129
+  \item {\tt SumE_fst} theorem, 130, 132, 144, 145
+  \item {\tt SumE_snd} theorem, 130, 132, 146
+  \item {\tt SumEL} theorem, 130
+  \item {\tt SumF} theorem, 130
+  \item {\tt SumFL} theorem, 130
+  \item {\tt SumI} theorem, 130, 140
+  \item {\tt SumIL} theorem, 130
+  \item {\tt SumIL2} theorem, 132
   \item {\tt surj} constant, 46, 71, 75
   \item {\tt surj_def} theorem, 46, 75
   \item {\tt surjective_pairing} theorem, 77
   \item {\tt surjective_sum} theorem, 79
   \item {\tt swap} theorem, 11, 66
-  \item {\tt swap_res_tac}, 16, 108
-  \item {\tt sym} theorem, 9, 65, 112
-  \item {\tt sym_elem} theorem, 125
-  \item {\tt sym_type} theorem, 125
-  \item {\tt symL} theorem, 113
+  \item {\tt swap_res_tac}, 16, 111
+  \item {\tt sym} theorem, 9, 65, 115
+  \item {\tt sym_elem} theorem, 128
+  \item {\tt sym_type} theorem, 128
+  \item {\tt symL} theorem, 116
 
   \indexspace
 
-  \item {\tt T} constant, 122
-  \item {\textit {t}} type, 121
+  \item {\tt T} constant, 125
+  \item {\textit {t}} type, 124
   \item {\tt take} constant, 82
   \item {\tt takeWhile} constant, 82
-  \item {\tt TC} theorem, 128
-  \item {\tt TE} theorem, 128
-  \item {\tt TEL} theorem, 128
-  \item {\tt term} class, 5, 61, 109
-  \item {\tt test_assume_tac}, \bold{130}
-  \item {\tt TF} theorem, 128
-  \item {\tt THE} symbol, 27, 29, 37, 110
-  \item {\tt The} constant, 26, 29, 30, 110
-  \item {\tt The} theorem, 112
+  \item {\tt TC} theorem, 131
+  \item {\tt TE} theorem, 131
+  \item {\tt TEL} theorem, 131
+  \item {\tt term} class, 5, 61, 112
+  \item {\tt test_assume_tac}, \bold{133}
+  \item {\tt TF} theorem, 131
+  \item {\tt THE} symbol, 27, 29, 37, 113
+  \item {\tt The} constant, 26, 29, 30, 113
+  \item {\tt The} theorem, 115
   \item {\tt the_def} theorem, 31
   \item {\tt the_equality} theorem, 36, 37
   \item {\tt theI} theorem, 36, 37
-  \item {\tt thinL} theorem, 112
-  \item {\tt thinR} theorem, 112
-  \item {\tt TI} theorem, 128
+  \item {\tt thinL} theorem, 115
+  \item {\tt thinR} theorem, 115
+  \item {\tt TI} theorem, 131
   \item {\tt times} class, 61
   \item {\tt tl} constant, 82
   \item tracing
     \subitem of unification, 62
-  \item {\tt trans} theorem, 9, 65, 112
-  \item {\tt trans_elem} theorem, 125
-  \item {\tt trans_red} theorem, 125
+  \item {\tt trans} theorem, 9, 65, 115
+  \item {\tt trans_elem} theorem, 128
+  \item {\tt trans_red} theorem, 128
   \item {\tt trans_tac}, 81
-  \item {\tt trans_type} theorem, 125
-  \item {\tt True} constant, 7, 60, 110
-  \item {\tt True_def} theorem, 8, 64, 112
+  \item {\tt trans_type} theorem, 128
+  \item {\tt True} constant, 7, 60, 113
+  \item {\tt True_def} theorem, 8, 64, 115
   \item {\tt True_or_False} theorem, 63, 64
   \item {\tt TrueI} theorem, 9, 65
-  \item {\tt Trueprop} constant, 7, 60, 110
-  \item {\tt TrueR} theorem, 113
-  \item {\tt tt} constant, 122
-  \item {\tt Type} constant, 122
+  \item {\tt Trueprop} constant, 7, 60, 113
+  \item {\tt TrueR} theorem, 116
+  \item {\tt tt} constant, 125
+  \item {\tt Type} constant, 125
   \item type definition, \bold{84}
-  \item {\tt typechk_tac}, \bold{130}, 135, 138, 142, 143
+  \item {\tt typechk_tac}, \bold{133}, 138, 141, 145, 146
   \item {\tt typedef}, 81
 
   \indexspace
@@ -942,7 +944,7 @@
 
   \indexspace
 
-  \item {\tt when} constant, 122, 127, 136
+  \item {\tt when} constant, 125, 130, 139
 
   \indexspace
 
@@ -950,7 +952,7 @@
 
   \indexspace
 
-  \item {\tt zero_ne_succ} theorem, 125, 126
+  \item {\tt zero_ne_succ} theorem, 128, 129
   \item {\tt ZF} theory, 1, 24, 59
   \item {\tt ZF_cs}, \bold{24}
   \item {\tt ZF_ss}, \bold{24}