1.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 21:41:11 2002 +0100
1.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 21:41:38 2002 +0100
1.3 @@ -9,11 +9,10 @@
1.4 %
1.5 \begin{isamarkuptext}%
1.6 Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate infrastructure
1.7 - for concrete syntax is that of general \emph{mixfix
1.8 - annotations}\index{mixfix annotations|bold}. Associated with any
1.9 - kind of name and type declaration, mixfixes give rise both to
1.10 - grammar productions for the parser and output templates for the
1.11 - pretty printer.
1.12 + for concrete syntax is that of general \bfindex{mixfix annotations}.
1.13 + Associated with any kind of name and type declaration, mixfixes give
1.14 + rise both to grammar productions for the parser and output templates
1.15 + for the pretty printer.
1.16
1.17 In full generality, the whole affair of parser and pretty printer
1.18 configuration is rather subtle. Any syntax specifications given by
1.19 @@ -28,7 +27,7 @@
1.20 \end{isamarkuptext}%
1.21 \isamarkuptrue%
1.22 %
1.23 -\isamarkupsubsection{Infixes%
1.24 +\isamarkupsubsection{Infix annotations%
1.25 }
1.26 \isamarkuptrue%
1.27 %
1.28 @@ -40,11 +39,11 @@
1.29 well, although this is less frequently encountered in practice
1.30 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
1.31
1.32 - Infix declarations\index{infix annotations|bold} provide a useful
1.33 - special case of mixfixes, where users need not care about the full
1.34 - details of priorities, nesting, spacing, etc. The subsequent
1.35 - example of the exclusive-or operation on boolean values illustrates
1.36 - typical infix declarations.%
1.37 + Infix declarations\index{infix annotations} provide a useful special
1.38 + case of mixfixes, where users need not care about the full details
1.39 + of priorities, nesting, spacing, etc. The subsequent example of the
1.40 + exclusive-or operation on boolean values illustrates typical infix
1.41 + declarations.%
1.42 \end{isamarkuptext}%
1.43 \isamarkuptrue%
1.44 \isacommand{constdefs}\isanewline
1.45 @@ -120,11 +119,10 @@
1.46 proposed over decades, but none has become universally available so
1.47 far, not even Unicode\index{Unicode}.
1.48
1.49 - Isabelle supports a generic notion of
1.50 - \emph{symbols}\index{symbols|bold} as the smallest entities of
1.51 - source text, without referring to internal encodings. Such
1.52 - ``generalized characters'' may be of one of the following three
1.53 - kinds:
1.54 + Isabelle supports a generic notion of \bfindex{symbols} as the
1.55 + smallest entities of source text, without referring to internal
1.56 + encodings. Such ``generalized characters'' may be of one of the
1.57 + following three kinds:
1.58
1.59 \begin{enumerate}
1.60
1.61 @@ -172,10 +170,10 @@
1.62 immediately after continuing further input.
1.63
1.64 \medskip A slightly more refined scheme is to provide alternative
1.65 - syntax via the \emph{print mode}\index{print mode} concept of
1.66 - Isabelle (see also \cite{isabelle-ref}). By convention, the mode
1.67 - ``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the
1.68 - following hybrid declaration of \isa{xor}.%
1.69 + syntax via the \bfindex{print mode} concept of Isabelle (see also
1.70 + \cite{isabelle-ref}). By convention, the mode ``$xsymbols$'' is
1.71 + enabled whenever X-Symbol is active. Consider the following hybrid
1.72 + declaration of \isa{xor}.%
1.73 \end{isamarkuptext}%
1.74 \isamarkuptrue%
1.75 \isamarkupfalse%
1.76 @@ -220,15 +218,15 @@
1.77 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
1.78 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
1.79 %
1.80 -\isamarkupsubsection{Prefixes%
1.81 +\isamarkupsubsection{Prefix annotations%
1.82 }
1.83 \isamarkuptrue%
1.84 %
1.85 \begin{isamarkuptext}%
1.86 -Prefix syntax annotations\index{prefix annotation|bold} are just a
1.87 - very degenerate of the general mixfix form \cite{isabelle-ref},
1.88 - without any template arguments or priorities --- just some piece of
1.89 - literal syntax.
1.90 +Prefix syntax annotations\index{prefix annotation} are just a very
1.91 + degenerate of the general mixfix form \cite{isabelle-ref}, without
1.92 + any template arguments or priorities --- just some piece of literal
1.93 + syntax.
1.94
1.95 The following example illustrates this idea idea by associating
1.96 common symbols with the constructors of a currency datatype.%
1.97 @@ -244,31 +242,25 @@
1.98 Here the degenerate mixfix annotations on the rightmost column
1.99 happen to consist of a single Isabelle symbol each:
1.100 \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
1.101 - \verb,\,\verb,<yen>,, and \verb,$,.
1.102 + \verb,\,\verb,<yen>,, \verb,$,.
1.103
1.104 Recall that a constructor like \isa{Euro} actually is a function
1.105 \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will
1.106 - be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Merely the head of the application is
1.107 - subject to our trivial concrete syntax; this form is sufficient to
1.108 - achieve fair conformance to EU~Commission standards of currency
1.109 - notation.
1.110 + be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Only the head of the application is
1.111 + subject to our concrete syntax; this simple form already achieves
1.112 + conformance with notational standards of the European Commission.
1.113
1.114 \medskip Certainly, the same idea of prefix syntax also works for
1.115 \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
1.116 might introduce a (slightly unrealistic) function to calculate an
1.117 abstract currency value, by cases on the datatype constructors and
1.118 - fixed exchange rates.%
1.119 + fixed exchange rates. The funny symbol used here is that of
1.120 + \verb,\<currency>,.%
1.121 \end{isamarkuptext}%
1.122 \isamarkuptrue%
1.123 \isacommand{consts}\isanewline
1.124 \ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
1.125 %
1.126 -\begin{isamarkuptext}%
1.127 -\noindent The funny symbol encountered here is that of
1.128 - \verb,\<currency>,.%
1.129 -\end{isamarkuptext}%
1.130 -\isamarkuptrue%
1.131 -%
1.132 \isamarkupsubsection{Syntax translations \label{sec:def-translations}%
1.133 }
1.134 \isamarkuptrue%
1.135 @@ -312,24 +304,250 @@
1.136 }
1.137 \isamarkuptrue%
1.138 %
1.139 -\isamarkupsubsection{Batch-mode sessions%
1.140 -}
1.141 +\begin{isamarkuptext}%
1.142 +Isabelle/Isar is centered around a certain notion of \bfindex{formal
1.143 + proof documents}\index{documents|bold}: ultimately the result of the
1.144 + user's theory development efforts is a human-readable record --- as
1.145 + a browsable PDF file or printed on paper. The overall document
1.146 + structure follows traditional mathematical articles, with
1.147 + sectioning, explanations, definitions, theorem statements, and
1.148 + proofs.
1.149 +
1.150 + The Isar proof language \cite{Wenzel-PhD}, which is not covered in
1.151 + this book, admits to write formal proof texts that are acceptable
1.152 + both to the machine and human readers at the same time. Thus
1.153 + marginal comments and explanations may be kept at a minimum.
1.154 + Nevertheless, Isabelle document output is still useful without
1.155 + actual Isar proof texts; formal specifications usually deserve their
1.156 + own coverage in the text, while unstructured proof scripts may be
1.157 + just ignore by readers (or intentionally suppressed from the text).
1.158 +
1.159 + \medskip The Isabelle document preparation system essentially acts
1.160 + like a formal front-end for {\LaTeX}. After checking definitions
1.161 + and proofs the theory sources are turned into typesetting
1.162 + instructions, so the final document is known to observe quite strong
1.163 + ``soundness'' properties. This enables users to write authentic
1.164 + reports on formal theory developments with little additional effort,
1.165 + the most tedious consistency checks are handled by the system.%
1.166 +\end{isamarkuptext}%
1.167 \isamarkuptrue%
1.168 %
1.169 -\isamarkupsubsection{{\LaTeX} macros%
1.170 -}
1.171 -\isamarkuptrue%
1.172 -%
1.173 -\isamarkupsubsubsection{Structure markup%
1.174 -}
1.175 -\isamarkuptrue%
1.176 -%
1.177 -\isamarkupsubsubsection{Symbols and characters%
1.178 +\isamarkupsubsection{Isabelle sessions%
1.179 }
1.180 \isamarkuptrue%
1.181 %
1.182 \begin{isamarkuptext}%
1.183 -FIXME%
1.184 +In contrast to the highly interactive mode of the formal parts of
1.185 + Isabelle/Isar theory development, the document preparation stage
1.186 + essentially works in batch-mode. This revolves around the concept
1.187 + of a \bfindex{session}, which essentially consists of a collection
1.188 + of theory source files that contribute to a single output document.
1.189 + Each session is derived from a parent one (usually an object-logic
1.190 + image such as \texttt{HOL}); this results in an overall tree
1.191 + structure of Isabelle sessions.
1.192 +
1.193 + The canonical arrangement of source files of a session called
1.194 + \texttt{MySession} is as follows:
1.195 +
1.196 + \begin{itemize}
1.197 +
1.198 + \item Directory \texttt{MySession} contains the required theory
1.199 + files, say $A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}.
1.200 +
1.201 + \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
1.202 + for loading all wanted theories, usually just
1.203 + \texttt{use_thy~"$A@i$"} for any $A@i$ in leaf position of the
1.204 + theory dependency graph.
1.205 +
1.206 + \item Directory \texttt{MySession/document} contains everything
1.207 + required for the {\LaTeX} stage, but only \texttt{root.tex} needs to
1.208 + be provided initially. The latter file holds appropriate {\LaTeX}
1.209 + code to commence a document (\verb,\documentclass, etc.), and to
1.210 + include the generated files $A@i$\texttt{.tex} for each theory. The
1.211 + generated file \texttt{session.tex} holds {\LaTeX} commands to
1.212 + include \emph{all} theory output files in topologically sorted
1.213 + order.
1.214 +
1.215 + \item In addition an \texttt{IsaMakefile} outside of directory
1.216 + \texttt{MySession} holds appropriate dependencies and invocations of
1.217 + Isabelle tools to control the batch job. The details are covered in
1.218 + \cite{isabelle-sys}; \texttt{isatool usedir} is the most important
1.219 + entry point.
1.220 +
1.221 + \end{itemize}
1.222 +
1.223 + With everything put in its proper place, \texttt{isatool make}
1.224 + should be sufficient to process the Isabelle session completely,
1.225 + with the generated document appearing in its proper place (within
1.226 + \verb,~/isabelle/browser_info,).
1.227 +
1.228 + In practive, users may want to have \texttt{isatool mkdir} generate
1.229 + an initial working setup without further ado. For example, an empty
1.230 + session \texttt{MySession} derived from \texttt{HOL} may be produced
1.231 + as follows:
1.232 +
1.233 +\begin{verbatim}
1.234 + isatool mkdir HOL MySession
1.235 + isatool make
1.236 +\end{verbatim}
1.237 +
1.238 + This runs the session with sensible default options, including
1.239 + verbose mode to tell the user where the result will appear. The
1.240 + above dry run should produce should produce a single page of output
1.241 + (with a dummy title, empty table of contents etc.). Any failure at
1.242 + that stage is likely to indicate some technical problems with your
1.243 + {\LaTeX} installation.\footnote{Especially make sure that
1.244 + \texttt{pdflatex} is present.}
1.245 +
1.246 + \medskip Users may now start to populate the directory
1.247 + \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
1.248 + accordingly. \texttt{MySession/document/root.tex} should be also
1.249 + adapted at some point; the generated version is mostly
1.250 + self-explanatory.
1.251 +
1.252 + Realistic applications may demand additional files in
1.253 + \texttt{MySession/document} for the {\LaTeX} stage, such as
1.254 + \texttt{root.bib} for the bibliographic database.\footnote{Using
1.255 + that particular name of \texttt{root.bib}, the Isabelle document
1.256 + processor (actually \texttt{isatool document} \cite{isabelle-sys})
1.257 + will be smart enough to invoke \texttt{bibtex} accordingly.}
1.258 +
1.259 + \medskip Failure of the document preparation phase in an Isabelle
1.260 + batch session leaves the generated sources in there target location
1.261 + (as pointed out by the accompanied error message). In case of
1.262 + {\LaTeX} errors, users may trace error messages at the file position
1.263 + of the generated text.%
1.264 +\end{isamarkuptext}%
1.265 +\isamarkuptrue%
1.266 +%
1.267 +\isamarkupsubsection{Structure markup%
1.268 +}
1.269 +\isamarkuptrue%
1.270 +%
1.271 +\isamarkupsubsubsection{Sections%
1.272 +}
1.273 +\isamarkuptrue%
1.274 +%
1.275 +\begin{isamarkuptext}%
1.276 +The large-scale structure of Isabelle documents closely follows
1.277 + {\LaTeX} convention, with chapters, sections, subsubsections etc.
1.278 + The formal Isar language includes separate structure \bfindex{markup
1.279 + commands}, which do not effect the formal content of a theory (or
1.280 + proof), but results in corresponding {\LaTeX} elements issued to the
1.281 + output.
1.282 +
1.283 + There are different markup commands for different formal contexts:
1.284 + in header position (just before a \isakeyword{theory} command),
1.285 + within the theory body, or within a proof. Note that the header
1.286 + needs to be treated specially, since ordinary theory and proof
1.287 + commands may only occur \emph{after} the initial \isakeyword{theory}
1.288 + specification.
1.289 +
1.290 + \smallskip
1.291 +
1.292 + \begin{tabular}{llll}
1.293 + header & theory & proof & default meaning \\\hline
1.294 + & \commdx{chapter} & & \verb,\chapter, \\
1.295 + \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
1.296 + & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
1.297 + & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
1.298 + \end{tabular}
1.299 +
1.300 + \medskip
1.301 +
1.302 + From the Isabelle perspective, each markup command takes a single
1.303 + text argument (delimited by \verb,",\dots\verb,", or
1.304 + \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping
1.305 + surrounding white space, the argument is passed to a {\LaTeX} macro
1.306 + \verb,\isamarkupXXX, for any command \isakeyword{XXX}. The latter
1.307 + are defined in \verb,isabelle.sty, according to the rightmost column
1.308 + above.
1.309 +
1.310 + \medskip The following source fragment illustrates structure markup
1.311 + of a theory.
1.312 +
1.313 + \begin{ttbox}
1.314 + header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
1.315 +
1.316 + theory Foo_Bar = Main:
1.317 +
1.318 + subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
1.319 +
1.320 + consts
1.321 + foo :: \dots
1.322 + bar :: \dots
1.323 + defs \dots
1.324 +
1.325 + subsection {\ttlbrace}* Derived rules *{\ttrbrace}
1.326 +
1.327 + lemma fooI: \dots
1.328 + lemma fooE: \dots
1.329 +
1.330 + subsection {\ttlbrace}* Main theorem *{\ttrbrace}
1.331 +
1.332 + theorem main: \dots
1.333 +
1.334 + end
1.335 + \end{ttbox}
1.336 +
1.337 + \medskip In realistic applications, users may well want to change
1.338 + the meaning of some markup commands, typically via appropriate use
1.339 + of \verb,\renewcommand, in \texttt{root.tex}. The
1.340 + \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\
1.341 + moving it up in the hierarchy to become \verb,\chapter,.
1.342 +
1.343 +\begin{verbatim}
1.344 + \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
1.345 +\end{verbatim}
1.346 +
1.347 + Certainly, this requires to change the default
1.348 + \verb,\documentclass{article}, in \texttt{root.tex} to something
1.349 + that supports the notion of chapters in the first place, e.g.\
1.350 + \texttt{report} or \texttt{book}.
1.351 +
1.352 + \medskip For each generated theory output the {\LaTeX} macro
1.353 + \verb,\isabellecontext, holds the name of the formal context. This
1.354 + is particularly useful for document headings or footings, e.g.\ like
1.355 + this:
1.356 +
1.357 +\begin{verbatim}
1.358 + \renewcommand{\isamarkupheader}[1]%
1.359 + {\chapter{#1}\markright{THEORY~\isabellecontext}}
1.360 +\end{verbatim}
1.361 +
1.362 + \noindent Make sure to include something like
1.363 + \verb,\pagestyle{headings}, in \texttt{root.tex} as well. Moreover,
1.364 + the document should have more than 2 pages.%
1.365 +\end{isamarkuptext}%
1.366 +\isamarkuptrue%
1.367 +%
1.368 +\isamarkupsubsection{Formal comments and antiquotations%
1.369 +}
1.370 +\isamarkuptrue%
1.371 +%
1.372 +\begin{isamarkuptext}%
1.373 +Comments of the form \verb,(*,~\dots~\verb,*),%
1.374 +\end{isamarkuptext}%
1.375 +\isamarkuptrue%
1.376 +%
1.377 +\isamarkupsubsection{Symbols and characters%
1.378 +}
1.379 +\isamarkuptrue%
1.380 +%
1.381 +\begin{isamarkuptext}%
1.382 +FIXME \verb,\isabellestyle,%
1.383 +\end{isamarkuptext}%
1.384 +\isamarkuptrue%
1.385 +%
1.386 +\isamarkupsubsection{Suppressing output%
1.387 +}
1.388 +\isamarkuptrue%
1.389 +%
1.390 +\begin{isamarkuptext}%
1.391 +FIXME \verb,no_document,
1.392 +
1.393 + FIXME \verb,(,\verb,*,\verb,<,\verb,*,\verb,),
1.394 + \verb,(,\verb,*,\verb,>,\verb,*,\verb,),%
1.395 \end{isamarkuptext}%
1.396 \isamarkuptrue%
1.397 \isamarkupfalse%
2.1 --- a/doc-src/TutorialI/tutorial.ind Sat Jan 05 21:41:11 2002 +0100
2.2 +++ b/doc-src/TutorialI/tutorial.ind Sat Jan 05 21:41:38 2002 +0100
2.3 @@ -1,661 +1,661 @@
2.4 \begin{theindex}
2.5
2.6 - \item \ttall, \bold{203}
2.7 - \item \texttt{?}, \bold{203}
2.8 - \item \isasymuniqex, \bold{203}
2.9 - \item \ttuniquex, \bold{203}
2.10 - \item {\texttt {\&}}, \bold{203}
2.11 - \item \verb$~$, \bold{203}
2.12 - \item \verb$~=$, \bold{203}
2.13 - \item \ttor, \bold{203}
2.14 + \item \ttall, \bold{207}
2.15 + \item \texttt{?}, \bold{207}
2.16 + \item \isasymuniqex, \bold{207}
2.17 + \item \ttuniquex, \bold{207}
2.18 + \item {\texttt {\&}}, \bold{207}
2.19 + \item \verb$~$, \bold{207}
2.20 + \item \verb$~=$, \bold{207}
2.21 + \item \ttor, \bold{207}
2.22 \item \texttt{[]}, \bold{9}
2.23 \item \texttt{\#}, \bold{9}
2.24 - \item \texttt{\at}, \bold{10}, \hyperpage{203}
2.25 - \item \isasymnotin, \bold{203}
2.26 - \item \verb$~:$, \bold{203}
2.27 - \item \isasymInter, \bold{203}
2.28 - \item \isasymUnion, \bold{203}
2.29 - \item \isasyminverse, \bold{203}
2.30 - \item \verb$^-1$, \bold{203}
2.31 - \item \isactrlsup{\isacharasterisk}, \bold{203}
2.32 - \item \verb$^$\texttt{*}, \bold{203}
2.33 - \item \isasymAnd, \bold{12}, \bold{203}
2.34 - \item \ttAnd, \bold{203}
2.35 - \item \isasymrightleftharpoons, \hyperpage{57}
2.36 - \item \isasymrightharpoonup, \hyperpage{57}
2.37 - \item \isasymleftharpoondown, \hyperpage{57}
2.38 + \item \texttt{\at}, \bold{10}, 207
2.39 + \item \isasymnotin, \bold{207}
2.40 + \item \verb$~:$, \bold{207}
2.41 + \item \isasymInter, \bold{207}
2.42 + \item \isasymUnion, \bold{207}
2.43 + \item \isasyminverse, \bold{207}
2.44 + \item \verb$^-1$, \bold{207}
2.45 + \item \isactrlsup{\isacharasterisk}, \bold{207}
2.46 + \item \verb$^$\texttt{*}, \bold{207}
2.47 + \item \isasymAnd, \bold{12}, \bold{207}
2.48 + \item \ttAnd, \bold{207}
2.49 + \item \isasymrightleftharpoons, 57
2.50 + \item \isasymrightharpoonup, 57
2.51 + \item \isasymleftharpoondown, 57
2.52 \item \emph {$\Rightarrow $}, \bold{5}
2.53 - \item \ttlbr, \bold{203}
2.54 - \item \ttrbr, \bold{203}
2.55 - \item \texttt {\%}, \bold{203}
2.56 + \item \ttlbr, \bold{207}
2.57 + \item \ttrbr, \bold{207}
2.58 + \item \texttt {\%}, \bold{207}
2.59 \item \texttt {;}, \bold{7}
2.60 - \item \isa {()} (constant), \hyperpage{24}
2.61 - \item \isa {+} (tactical), \hyperpage{93}
2.62 + \item \isa {()} (constant), 24
2.63 + \item \isa {+} (tactical), 97
2.64 \item \isa {<*lex*>}, \see{lexicographic product}{1}
2.65 - \item \isa {?} (tactical), \hyperpage{93}
2.66 - \item \texttt{|} (tactical), \hyperpage{93}
2.67 + \item \isa {?} (tactical), 97
2.68 + \item \texttt{|} (tactical), 97
2.69
2.70 \indexspace
2.71
2.72 - \item \isa {0} (constant), \hyperpage{22, 23}, \hyperpage{144}
2.73 - \item \isa {1} (constant), \hyperpage{23}, \hyperpage{144, 145}
2.74 + \item \isa {0} (constant), 22, 23, 148
2.75 + \item \isa {1} (constant), 23, 148, 149
2.76
2.77 \indexspace
2.78
2.79 \item abandoning a proof, \bold{13}
2.80 \item abandoning a theory, \bold{16}
2.81 - \item \isa {abs} (constant), \hyperpage{147}
2.82 - \item \texttt {abs}, \bold{203}
2.83 - \item absolute value, \hyperpage{147}
2.84 - \item \isa {add} (modifier), \hyperpage{29}
2.85 - \item \isa {add_ac} (theorems), \hyperpage{146}
2.86 - \item \isa {add_assoc} (theorem), \bold{146}
2.87 - \item \isa {add_commute} (theorem), \bold{146}
2.88 - \item \isa {add_mult_distrib} (theorem), \bold{145}
2.89 - \item \texttt {ALL}, \bold{203}
2.90 - \item \isa {All} (constant), \hyperpage{103}
2.91 - \item \isa {allE} (theorem), \bold{75}
2.92 - \item \isa {allI} (theorem), \bold{74}
2.93 - \item append function, \hyperpage{10--14}
2.94 - \item \isacommand {apply} (command), \hyperpage{15}
2.95 - \item \isa {arg_cong} (theorem), \bold{90}
2.96 - \item \isa {arith} (method), \hyperpage{23}, \hyperpage{143}
2.97 + \item \isa {abs} (constant), 151
2.98 + \item \texttt {abs}, \bold{207}
2.99 + \item absolute value, 151
2.100 + \item \isa {add} (modifier), 29
2.101 + \item \isa {add_ac} (theorems), 150
2.102 + \item \isa {add_assoc} (theorem), \bold{150}
2.103 + \item \isa {add_commute} (theorem), \bold{150}
2.104 + \item \isa {add_mult_distrib} (theorem), \bold{149}
2.105 + \item \texttt {ALL}, \bold{207}
2.106 + \item \isa {All} (constant), 107
2.107 + \item \isa {allE} (theorem), \bold{79}
2.108 + \item \isa {allI} (theorem), \bold{78}
2.109 + \item append function, 10--14
2.110 + \item \isacommand {apply} (command), 15
2.111 + \item \isa {arg_cong} (theorem), \bold{94}
2.112 + \item \isa {arith} (method), 23, 147
2.113 \item arithmetic operations
2.114 - \subitem for \protect\isa{nat}, \hyperpage{23}
2.115 - \item \textsc {ascii} symbols, \bold{203}
2.116 - \item Aspinall, David, \hyperpage{viii}
2.117 - \item associative-commutative function, \hyperpage{170}
2.118 - \item \isa {assumption} (method), \hyperpage{63}
2.119 + \subitem for \protect\isa{nat}, 23
2.120 + \item \textsc {ascii} symbols, \bold{207}
2.121 + \item Aspinall, David, viii
2.122 + \item associative-commutative function, 174
2.123 + \item \isa {assumption} (method), 67
2.124 \item assumptions
2.125 - \subitem of subgoal, \hyperpage{12}
2.126 - \subitem renaming, \hyperpage{76--77}
2.127 - \subitem reusing, \hyperpage{77}
2.128 - \item \isa {auto} (method), \hyperpage{38}, \hyperpage{86}
2.129 - \item \isa {axclass}, \hyperpage{158--164}
2.130 - \item axiom of choice, \hyperpage{80}
2.131 - \item axiomatic type classes, \hyperpage{158--164}
2.132 + \subitem of subgoal, 12
2.133 + \subitem renaming, 80--81
2.134 + \subitem reusing, 81
2.135 + \item \isa {auto} (method), 38, 90
2.136 + \item \isa {axclass}, 162--168
2.137 + \item axiom of choice, 84
2.138 + \item axiomatic type classes, 162--168
2.139
2.140 \indexspace
2.141
2.142 - \item \isacommand {back} (command), \hyperpage{72}
2.143 - \item \isa {Ball} (constant), \hyperpage{103}
2.144 - \item \isa {ballI} (theorem), \bold{102}
2.145 - \item \isa {best} (method), \hyperpage{86}
2.146 - \item \isa {Bex} (constant), \hyperpage{103}
2.147 - \item \isa {bexE} (theorem), \bold{102}
2.148 - \item \isa {bexI} (theorem), \bold{102}
2.149 - \item \isa {bij_def} (theorem), \bold{104}
2.150 - \item bijections, \hyperpage{104}
2.151 - \item binary trees, \hyperpage{18}
2.152 - \item binomial coefficients, \hyperpage{103}
2.153 - \item bisimulations, \hyperpage{110}
2.154 - \item \isa {blast} (method), \hyperpage{83--84}, \hyperpage{86}
2.155 - \item \isa {bool} (type), \hyperpage{4, 5}
2.156 - \item boolean expressions example, \hyperpage{20--22}
2.157 - \item \isa {bspec} (theorem), \bold{102}
2.158 - \item \isacommand{by} (command), \hyperpage{67}
2.159 + \item \isacommand {back} (command), 76
2.160 + \item \isa {Ball} (constant), 107
2.161 + \item \isa {ballI} (theorem), \bold{106}
2.162 + \item \isa {best} (method), 90
2.163 + \item \isa {Bex} (constant), 107
2.164 + \item \isa {bexE} (theorem), \bold{106}
2.165 + \item \isa {bexI} (theorem), \bold{106}
2.166 + \item \isa {bij_def} (theorem), \bold{108}
2.167 + \item bijections, 108
2.168 + \item binary trees, 18
2.169 + \item binomial coefficients, 107
2.170 + \item bisimulations, 114
2.171 + \item \isa {blast} (method), 87--88, 90
2.172 + \item \isa {bool} (type), 4, 5
2.173 + \item boolean expressions example, 20--22
2.174 + \item \isa {bspec} (theorem), \bold{106}
2.175 + \item \isacommand{by} (command), 71
2.176
2.177 \indexspace
2.178
2.179 - \item \isa {card} (constant), \hyperpage{103}
2.180 - \item \isa {card_Pow} (theorem), \bold{103}
2.181 - \item \isa {card_Un_Int} (theorem), \bold{103}
2.182 - \item cardinality, \hyperpage{103}
2.183 - \item \isa {case} (symbol), \hyperpage{32, 33}
2.184 - \item \isa {case} expressions, \hyperpage{5, 6}, \hyperpage{18}
2.185 - \item case distinctions, \hyperpage{19}
2.186 + \item \isa {card} (constant), 107
2.187 + \item \isa {card_Pow} (theorem), \bold{107}
2.188 + \item \isa {card_Un_Int} (theorem), \bold{107}
2.189 + \item cardinality, 107
2.190 + \item \isa {case} (symbol), 32, 33
2.191 + \item \isa {case} expressions, 5, 6, 18
2.192 + \item case distinctions, 19
2.193 \item case splits, \bold{31}
2.194 - \item \isa {case_tac} (method), \hyperpage{19}, \hyperpage{95},
2.195 - \hyperpage{151}
2.196 - \item \isa {cases} (method), \hyperpage{156}
2.197 - \item \isa {clarify} (method), \hyperpage{85, 86}
2.198 - \item \isa {clarsimp} (method), \hyperpage{85, 86}
2.199 - \item \isa {classical} (theorem), \bold{67}
2.200 - \item coinduction, \bold{110}
2.201 - \item \isa {Collect} (constant), \hyperpage{103}
2.202 - \item compiling expressions example, \hyperpage{36--38}
2.203 - \item \isa {Compl_iff} (theorem), \bold{100}
2.204 + \item \isa {case_tac} (method), 19, 99, 155
2.205 + \item \isa {cases} (method), 160
2.206 + \item \isacommand {chapter} (command), 59
2.207 + \item \isa {clarify} (method), 89, 90
2.208 + \item \isa {clarsimp} (method), 89, 90
2.209 + \item \isa {classical} (theorem), \bold{71}
2.210 + \item coinduction, \bold{114}
2.211 + \item \isa {Collect} (constant), 107
2.212 + \item compiling expressions example, 36--38
2.213 + \item \isa {Compl_iff} (theorem), \bold{104}
2.214 \item complement
2.215 - \subitem of a set, \hyperpage{99}
2.216 + \subitem of a set, 103
2.217 \item composition
2.218 - \subitem of functions, \bold{104}
2.219 - \subitem of relations, \bold{106}
2.220 + \subitem of functions, \bold{108}
2.221 + \subitem of relations, \bold{110}
2.222 \item conclusion
2.223 - \subitem of subgoal, \hyperpage{12}
2.224 + \subitem of subgoal, 12
2.225 \item conditional expressions, \see{\isa{if} expressions}{1}
2.226 - \item conditional simplification rules, \hyperpage{31}
2.227 - \item \isa {cong} (attribute), \hyperpage{170}
2.228 - \item congruence rules, \bold{169}
2.229 - \item \isa {conjE} (theorem), \bold{65}
2.230 - \item \isa {conjI} (theorem), \bold{62}
2.231 - \item \isa {Cons} (constant), \hyperpage{9}
2.232 - \item \isacommand {constdefs} (command), \hyperpage{25}
2.233 - \item \isacommand {consts} (command), \hyperpage{10}
2.234 - \item contrapositives, \hyperpage{67}
2.235 + \item conditional simplification rules, 31
2.236 + \item \isa {cong} (attribute), 174
2.237 + \item congruence rules, \bold{173}
2.238 + \item \isa {conjE} (theorem), \bold{69}
2.239 + \item \isa {conjI} (theorem), \bold{66}
2.240 + \item \isa {Cons} (constant), 9
2.241 + \item \isacommand {constdefs} (command), 25
2.242 + \item \isacommand {consts} (command), 10
2.243 + \item contrapositives, 71
2.244 \item converse
2.245 - \subitem of a relation, \bold{106}
2.246 - \item \isa {converse_iff} (theorem), \bold{106}
2.247 - \item CTL, \hyperpage{115--120}, \hyperpage{185--187}
2.248 + \subitem of a relation, \bold{110}
2.249 + \item \isa {converse_iff} (theorem), \bold{110}
2.250 + \item CTL, 119--124, 189--191
2.251
2.252 \indexspace
2.253
2.254 - \item \isacommand {datatype} (command), \hyperpage{9},
2.255 - \hyperpage{38--43}
2.256 - \item datatypes, \hyperpage{17--22}
2.257 - \subitem and nested recursion, \hyperpage{40}, \hyperpage{44}
2.258 - \subitem mutually recursive, \hyperpage{38}
2.259 - \subitem nested, \hyperpage{174}
2.260 - \item \isacommand {defer} (command), \hyperpage{16}, \hyperpage{94}
2.261 - \item Definitional Approach, \hyperpage{26}
2.262 + \item \isacommand {datatype} (command), 9, 38--43
2.263 + \item datatypes, 17--22
2.264 + \subitem and nested recursion, 40, 44
2.265 + \subitem mutually recursive, 38
2.266 + \subitem nested, 178
2.267 + \item \isacommand {defer} (command), 16, 98
2.268 + \item Definitional Approach, 26
2.269 \item definitions, \bold{25}
2.270 \subitem unfolding, \bold{30}
2.271 - \item \isacommand {defs} (command), \hyperpage{25}
2.272 - \item \isa {del} (modifier), \hyperpage{29}
2.273 - \item description operators, \hyperpage{79--81}
2.274 + \item \isacommand {defs} (command), 25
2.275 + \item \isa {del} (modifier), 29
2.276 + \item description operators, 83--85
2.277 \item descriptions
2.278 - \subitem definite, \hyperpage{79}
2.279 - \subitem indefinite, \hyperpage{80}
2.280 - \item \isa {dest} (attribute), \hyperpage{96}
2.281 - \item destruction rules, \hyperpage{65}
2.282 - \item \isa {diff_mult_distrib} (theorem), \bold{145}
2.283 + \subitem definite, 83
2.284 + \subitem indefinite, 84
2.285 + \item \isa {dest} (attribute), 100
2.286 + \item destruction rules, 69
2.287 + \item \isa {diff_mult_distrib} (theorem), \bold{149}
2.288 \item difference
2.289 - \subitem of sets, \bold{100}
2.290 - \item \isa {disjCI} (theorem), \bold{68}
2.291 - \item \isa {disjE} (theorem), \bold{64}
2.292 - \item \isa {div} (symbol), \hyperpage{23}
2.293 - \item divides relation, \hyperpage{78}, \hyperpage{89},
2.294 - \hyperpage{95--98}, \hyperpage{146}
2.295 + \subitem of sets, \bold{104}
2.296 + \item \isa {disjCI} (theorem), \bold{72}
2.297 + \item \isa {disjE} (theorem), \bold{68}
2.298 + \item \isa {div} (symbol), 23
2.299 + \item divides relation, 82, 93, 99--102, 150
2.300 \item division
2.301 - \subitem by negative numbers, \hyperpage{147}
2.302 - \subitem by zero, \hyperpage{146}
2.303 - \subitem for type \protect\isa{nat}, \hyperpage{145}
2.304 + \subitem by negative numbers, 151
2.305 + \subitem by zero, 150
2.306 + \subitem for type \protect\isa{nat}, 149
2.307 + \item documents, \bold{57}
2.308 \item domain
2.309 - \subitem of a relation, \hyperpage{106}
2.310 - \item \isa {Domain_iff} (theorem), \bold{106}
2.311 - \item \isacommand {done} (command), \hyperpage{13}
2.312 - \item \isa {drule_tac} (method), \hyperpage{70}, \hyperpage{90}
2.313 - \item \isa {dvd_add} (theorem), \bold{146}
2.314 - \item \isa {dvd_anti_sym} (theorem), \bold{146}
2.315 - \item \isa {dvd_def} (theorem), \bold{146}
2.316 + \subitem of a relation, 110
2.317 + \item \isa {Domain_iff} (theorem), \bold{110}
2.318 + \item \isacommand {done} (command), 13
2.319 + \item \isa {drule_tac} (method), 74, 94
2.320 + \item \isa {dvd_add} (theorem), \bold{150}
2.321 + \item \isa {dvd_anti_sym} (theorem), \bold{150}
2.322 + \item \isa {dvd_def} (theorem), \bold{150}
2.323
2.324 \indexspace
2.325
2.326 - \item \isa {elim!} (attribute), \hyperpage{125}
2.327 - \item elimination rules, \hyperpage{63--64}
2.328 - \item \isacommand {end} (command), \hyperpage{14}
2.329 - \item \isa {Eps} (constant), \hyperpage{103}
2.330 - \item equality, \hyperpage{5}
2.331 - \subitem of functions, \bold{103}
2.332 - \subitem of records, \hyperpage{155}
2.333 - \subitem of sets, \bold{100}
2.334 - \item \isa {equalityE} (theorem), \bold{100}
2.335 - \item \isa {equalityI} (theorem), \bold{100}
2.336 - \item \isa {erule} (method), \hyperpage{64}
2.337 - \item \isa {erule_tac} (method), \hyperpage{70}
2.338 - \item Euclid's algorithm, \hyperpage{95--98}
2.339 + \item \isa {elim!} (attribute), 129
2.340 + \item elimination rules, 67--68
2.341 + \item \isacommand {end} (command), 14
2.342 + \item \isa {Eps} (constant), 107
2.343 + \item equality, 5
2.344 + \subitem of functions, \bold{107}
2.345 + \subitem of records, 159
2.346 + \subitem of sets, \bold{104}
2.347 + \item \isa {equalityE} (theorem), \bold{104}
2.348 + \item \isa {equalityI} (theorem), \bold{104}
2.349 + \item \isa {erule} (method), 68
2.350 + \item \isa {erule_tac} (method), 74
2.351 + \item Euclid's algorithm, 99--102
2.352 \item even numbers
2.353 - \subitem defining inductively, \hyperpage{121--125}
2.354 - \item \texttt {EX}, \bold{203}
2.355 - \item \isa {Ex} (constant), \hyperpage{103}
2.356 - \item \isa {exE} (theorem), \bold{76}
2.357 - \item \isa {exI} (theorem), \bold{76}
2.358 - \item \isa {ext} (theorem), \bold{103}
2.359 - \item \isa {extend} (constant), \hyperpage{157}
2.360 + \subitem defining inductively, 125--129
2.361 + \item \texttt {EX}, \bold{207}
2.362 + \item \isa {Ex} (constant), 107
2.363 + \item \isa {exE} (theorem), \bold{80}
2.364 + \item \isa {exI} (theorem), \bold{80}
2.365 + \item \isa {ext} (theorem), \bold{107}
2.366 + \item \isa {extend} (constant), 161
2.367 \item extensionality
2.368 - \subitem for functions, \bold{103, 104}
2.369 - \subitem for records, \hyperpage{155}
2.370 - \subitem for sets, \bold{100}
2.371 - \item \ttEXU, \bold{203}
2.372 + \subitem for functions, \bold{107, 108}
2.373 + \subitem for records, 159
2.374 + \subitem for sets, \bold{104}
2.375 + \item \ttEXU, \bold{207}
2.376
2.377 \indexspace
2.378
2.379 - \item \isa {False} (constant), \hyperpage{5}
2.380 - \item \isa {fast} (method), \hyperpage{86}, \hyperpage{118}
2.381 - \item Fibonacci function, \hyperpage{47}
2.382 - \item \isa {fields} (constant), \hyperpage{157}
2.383 - \item \isa {finite} (symbol), \hyperpage{103}
2.384 - \item \isa {Finites} (constant), \hyperpage{103}
2.385 - \item fixed points, \hyperpage{110}
2.386 - \item flags, \hyperpage{5, 6}, \hyperpage{33}
2.387 - \subitem setting and resetting, \hyperpage{5}
2.388 - \item \isa {force} (method), \hyperpage{85, 86}
2.389 - \item formulae, \hyperpage{5--6}
2.390 - \item forward proof, \hyperpage{86--92}
2.391 - \item \isa {frule} (method), \hyperpage{77}
2.392 - \item \isa {frule_tac} (method), \hyperpage{70}
2.393 - \item \isa {fst} (constant), \hyperpage{24}
2.394 - \item function types, \hyperpage{5}
2.395 - \item functions, \hyperpage{103--105}
2.396 - \subitem partial, \hyperpage{176}
2.397 - \subitem total, \hyperpage{11}, \hyperpage{46--52}
2.398 - \subitem underdefined, \hyperpage{177}
2.399 + \item \isa {False} (constant), 5
2.400 + \item \isa {fast} (method), 90, 122
2.401 + \item Fibonacci function, 47
2.402 + \item \isa {fields} (constant), 161
2.403 + \item \isa {finite} (symbol), 107
2.404 + \item \isa {Finites} (constant), 107
2.405 + \item fixed points, 114
2.406 + \item flags, 5, 6, 33
2.407 + \subitem setting and resetting, 5
2.408 + \item \isa {force} (method), 89, 90
2.409 + \item formal proof documents, \bold{57}
2.410 + \item formulae, 5--6
2.411 + \item forward proof, 90--96
2.412 + \item \isa {frule} (method), 81
2.413 + \item \isa {frule_tac} (method), 74
2.414 + \item \isa {fst} (constant), 24
2.415 + \item function types, 5
2.416 + \item functions, 107--109
2.417 + \subitem partial, 180
2.418 + \subitem total, 11, 46--52
2.419 + \subitem underdefined, 181
2.420
2.421 \indexspace
2.422
2.423 - \item \isa {gcd} (constant), \hyperpage{87--88}, \hyperpage{95--98}
2.424 - \item generalizing for induction, \hyperpage{123}
2.425 - \item generalizing induction formulae, \hyperpage{35}
2.426 - \item Girard, Jean-Yves, \fnote{65}
2.427 - \item Gordon, Mike, \hyperpage{3}
2.428 + \item \isa {gcd} (constant), 91--92, 99--102
2.429 + \item generalizing for induction, 127
2.430 + \item generalizing induction formulae, 35
2.431 + \item Girard, Jean-Yves, \fnote{69}
2.432 + \item Gordon, Mike, 3
2.433 \item grammars
2.434 - \subitem defining inductively, \hyperpage{134--139}
2.435 - \item ground terms example, \hyperpage{129--134}
2.436 + \subitem defining inductively, 138--143
2.437 + \item ground terms example, 133--138
2.438
2.439 \indexspace
2.440
2.441 - \item \isa {hd} (constant), \hyperpage{17}, \hyperpage{37}
2.442 - \item Hilbert's $\varepsilon$-operator, \hyperpage{80}
2.443 - \item HOLCF, \hyperpage{43}
2.444 - \item Hopcroft, J. E., \hyperpage{139}
2.445 - \item \isa {hypreal} (type), \hyperpage{149}
2.446 + \item \isa {hd} (constant), 17, 37
2.447 + \item \isacommand {header} (command), 59
2.448 + \item Hilbert's $\varepsilon$-operator, 84
2.449 + \item HOLCF, 43
2.450 + \item Hopcroft, J. E., 143
2.451 + \item \isa {hypreal} (type), 153
2.452
2.453 \indexspace
2.454
2.455 - \item \isa {Id_def} (theorem), \bold{106}
2.456 - \item \isa {id_def} (theorem), \bold{104}
2.457 + \item \isa {Id_def} (theorem), \bold{110}
2.458 + \item \isa {id_def} (theorem), \bold{108}
2.459 \item identifiers, \bold{6}
2.460 \subitem qualified, \bold{4}
2.461 - \item identity function, \bold{104}
2.462 - \item identity relation, \bold{106}
2.463 - \item \isa {if} expressions, \hyperpage{5, 6}
2.464 - \subitem simplification of, \hyperpage{33}
2.465 - \subitem splitting of, \hyperpage{31}, \hyperpage{49}
2.466 - \item if-and-only-if, \hyperpage{6}
2.467 - \item \isa {iff} (attribute), \hyperpage{84}, \hyperpage{96},
2.468 - \hyperpage{124}
2.469 - \item \isa {iffD1} (theorem), \bold{88}
2.470 - \item \isa {iffD2} (theorem), \bold{88}
2.471 + \item identity function, \bold{108}
2.472 + \item identity relation, \bold{110}
2.473 + \item \isa {if} expressions, 5, 6
2.474 + \subitem simplification of, 33
2.475 + \subitem splitting of, 31, 49
2.476 + \item if-and-only-if, 6
2.477 + \item \isa {iff} (attribute), 88, 100, 128
2.478 + \item \isa {iffD1} (theorem), \bold{92}
2.479 + \item \isa {iffD2} (theorem), \bold{92}
2.480 \item image
2.481 - \subitem under a function, \bold{105}
2.482 - \subitem under a relation, \bold{106}
2.483 - \item \isa {image_def} (theorem), \bold{105}
2.484 - \item \isa {Image_iff} (theorem), \bold{106}
2.485 - \item \isa {impI} (theorem), \bold{66}
2.486 - \item implication, \hyperpage{66--67}
2.487 - \item \isa {ind_cases} (method), \hyperpage{125}
2.488 - \item \isa {induct_tac} (method), \hyperpage{12}, \hyperpage{19},
2.489 - \hyperpage{52}, \hyperpage{184}
2.490 - \item induction, \hyperpage{180--187}
2.491 - \subitem complete, \hyperpage{182}
2.492 - \subitem deriving new schemas, \hyperpage{184}
2.493 - \subitem on a term, \hyperpage{181}
2.494 - \subitem recursion, \hyperpage{51--52}
2.495 - \subitem structural, \hyperpage{19}
2.496 - \subitem well-founded, \hyperpage{109}
2.497 - \item induction heuristics, \hyperpage{34--36}
2.498 - \item \isacommand {inductive} (command), \hyperpage{121}
2.499 + \subitem under a function, \bold{109}
2.500 + \subitem under a relation, \bold{110}
2.501 + \item \isa {image_def} (theorem), \bold{109}
2.502 + \item \isa {Image_iff} (theorem), \bold{110}
2.503 + \item \isa {impI} (theorem), \bold{70}
2.504 + \item implication, 70--71
2.505 + \item \isa {ind_cases} (method), 129
2.506 + \item \isa {induct_tac} (method), 12, 19, 52, 188
2.507 + \item induction, 184--191
2.508 + \subitem complete, 186
2.509 + \subitem deriving new schemas, 188
2.510 + \subitem on a term, 185
2.511 + \subitem recursion, 51--52
2.512 + \subitem structural, 19
2.513 + \subitem well-founded, 113
2.514 + \item induction heuristics, 34--36
2.515 + \item \isacommand {inductive} (command), 125
2.516 \item inductive definition
2.517 - \subitem simultaneous, \hyperpage{135}
2.518 - \item inductive definitions, \hyperpage{121--139}
2.519 - \item \isacommand {inductive\_cases} (command), \hyperpage{125},
2.520 - \hyperpage{133}
2.521 - \item infinitely branching trees, \hyperpage{43}
2.522 - \item infix annotations, \bold{54}
2.523 - \item \isacommand{infixr} (annotation), \hyperpage{10}
2.524 - \item \isa {inj_on_def} (theorem), \bold{104}
2.525 - \item injections, \hyperpage{104}
2.526 - \item \isa {insert} (constant), \hyperpage{101}
2.527 - \item \isa {insert} (method), \hyperpage{91--92}
2.528 - \item instance, \bold{160}
2.529 - \item \texttt {INT}, \bold{203}
2.530 - \item \texttt {Int}, \bold{203}
2.531 - \item \isa {int} (type), \hyperpage{147--148}
2.532 - \item \isa {INT_iff} (theorem), \bold{102}
2.533 - \item \isa {IntD1} (theorem), \bold{99}
2.534 - \item \isa {IntD2} (theorem), \bold{99}
2.535 - \item integers, \hyperpage{147--148}
2.536 - \item \isa {INTER} (constant), \hyperpage{103}
2.537 - \item \texttt {Inter}, \bold{203}
2.538 - \item \isa {Inter_iff} (theorem), \bold{102}
2.539 - \item intersection, \hyperpage{99}
2.540 - \subitem indexed, \hyperpage{102}
2.541 - \item \isa {IntI} (theorem), \bold{99}
2.542 - \item \isa {intro} (method), \hyperpage{68}
2.543 - \item \isa {intro!} (attribute), \hyperpage{122}
2.544 - \item \isa {intro_classes} (method), \hyperpage{160}
2.545 - \item introduction rules, \hyperpage{62--63}
2.546 - \item \isa {inv} (constant), \hyperpage{80}
2.547 - \item \isa {inv_image_def} (theorem), \bold{109}
2.548 + \subitem simultaneous, 139
2.549 + \item inductive definitions, 125--143
2.550 + \item \isacommand {inductive\_cases} (command), 129, 137
2.551 + \item infinitely branching trees, 43
2.552 + \item infix annotations, 54
2.553 + \item \isacommand{infixr} (annotation), 10
2.554 + \item \isa {inj_on_def} (theorem), \bold{108}
2.555 + \item injections, 108
2.556 + \item \isa {insert} (constant), 105
2.557 + \item \isa {insert} (method), 95--96
2.558 + \item instance, \bold{164}
2.559 + \item \texttt {INT}, \bold{207}
2.560 + \item \texttt {Int}, \bold{207}
2.561 + \item \isa {int} (type), 151--152
2.562 + \item \isa {INT_iff} (theorem), \bold{106}
2.563 + \item \isa {IntD1} (theorem), \bold{103}
2.564 + \item \isa {IntD2} (theorem), \bold{103}
2.565 + \item integers, 151--152
2.566 + \item \isa {INTER} (constant), 107
2.567 + \item \texttt {Inter}, \bold{207}
2.568 + \item \isa {Inter_iff} (theorem), \bold{106}
2.569 + \item intersection, 103
2.570 + \subitem indexed, 106
2.571 + \item \isa {IntI} (theorem), \bold{103}
2.572 + \item \isa {intro} (method), 72
2.573 + \item \isa {intro!} (attribute), 126
2.574 + \item \isa {intro_classes} (method), 164
2.575 + \item introduction rules, 66--67
2.576 + \item \isa {inv} (constant), 84
2.577 + \item \isa {inv_image_def} (theorem), \bold{113}
2.578 \item inverse
2.579 - \subitem of a function, \bold{104}
2.580 - \subitem of a relation, \bold{106}
2.581 + \subitem of a function, \bold{108}
2.582 + \subitem of a relation, \bold{110}
2.583 \item inverse image
2.584 - \subitem of a function, \hyperpage{105}
2.585 - \subitem of a relation, \hyperpage{108}
2.586 - \item \isa {itrev} (constant), \hyperpage{34}
2.587 + \subitem of a function, 109
2.588 + \subitem of a relation, 112
2.589 + \item \isa {itrev} (constant), 34
2.590
2.591 \indexspace
2.592
2.593 - \item \isacommand {kill} (command), \hyperpage{16}
2.594 + \item \isacommand {kill} (command), 16
2.595
2.596 \indexspace
2.597
2.598 - \item $\lambda$ expressions, \hyperpage{5}
2.599 - \item LCF, \hyperpage{43}
2.600 - \item \isa {LEAST} (symbol), \hyperpage{23}, \hyperpage{79}
2.601 - \item least number operator, \see{\protect\isa{LEAST}}{79}
2.602 - \item Leibniz, Gottfried Wilhelm, \hyperpage{53}
2.603 - \item \isacommand {lemma} (command), \hyperpage{13}
2.604 - \item \isacommand {lemmas} (command), \hyperpage{87}, \hyperpage{96}
2.605 - \item \isa {length} (symbol), \hyperpage{18}
2.606 - \item \isa {length_induct}, \bold{184}
2.607 - \item \isa {less_than} (constant), \hyperpage{108}
2.608 - \item \isa {less_than_iff} (theorem), \bold{108}
2.609 - \item \isa {let} expressions, \hyperpage{5, 6}, \hyperpage{31}
2.610 - \item \isa {Let_def} (theorem), \hyperpage{31}
2.611 - \item \isa {lex_prod_def} (theorem), \bold{109}
2.612 - \item lexicographic product, \bold{109}, \hyperpage{172}
2.613 + \item $\lambda$ expressions, 5
2.614 + \item LCF, 43
2.615 + \item \isa {LEAST} (symbol), 23, 83
2.616 + \item least number operator, \see{\protect\isa{LEAST}}{83}
2.617 + \item Leibniz, Gottfried Wilhelm, 53
2.618 + \item \isacommand {lemma} (command), 13
2.619 + \item \isacommand {lemmas} (command), 91, 100
2.620 + \item \isa {length} (symbol), 18
2.621 + \item \isa {length_induct}, \bold{188}
2.622 + \item \isa {less_than} (constant), 112
2.623 + \item \isa {less_than_iff} (theorem), \bold{112}
2.624 + \item \isa {let} expressions, 5, 6, 31
2.625 + \item \isa {Let_def} (theorem), 31
2.626 + \item \isa {lex_prod_def} (theorem), \bold{113}
2.627 + \item lexicographic product, \bold{113}, 176
2.628 \item {\texttt{lfp}}
2.629 - \subitem applications of, \see{CTL}{110}
2.630 - \item Library, \hyperpage{4}
2.631 - \item linear arithmetic, \hyperpage{22--24}, \hyperpage{143}
2.632 - \item \isa {List} (theory), \hyperpage{17}
2.633 - \item \isa {list} (type), \hyperpage{5}, \hyperpage{9},
2.634 - \hyperpage{17}
2.635 - \item \isa {list.split} (theorem), \hyperpage{32}
2.636 - \item \isa {lists_mono} (theorem), \bold{131}
2.637 - \item Lowe, Gavin, \hyperpage{190--191}
2.638 + \subitem applications of, \see{CTL}{114}
2.639 + \item Library, 4
2.640 + \item linear arithmetic, 22--24, 147
2.641 + \item \isa {List} (theory), 17
2.642 + \item \isa {list} (type), 5, 9, 17
2.643 + \item \isa {list.split} (theorem), 32
2.644 + \item \isa {lists_mono} (theorem), \bold{135}
2.645 + \item Lowe, Gavin, 194--195
2.646
2.647 \indexspace
2.648
2.649 - \item \isa {Main} (theory), \hyperpage{4}
2.650 - \item major premise, \bold{69}
2.651 - \item \isa {make} (constant), \hyperpage{157}
2.652 - \item \isa {max} (constant), \hyperpage{23, 24}
2.653 - \item measure functions, \hyperpage{47}, \hyperpage{108}
2.654 - \item \isa {measure_def} (theorem), \bold{109}
2.655 - \item meta-logic, \bold{74}
2.656 + \item \isa {Main} (theory), 4
2.657 + \item major premise, \bold{73}
2.658 + \item \isa {make} (constant), 161
2.659 + \item markup commands, \bold{59}
2.660 + \item \isa {max} (constant), 23, 24
2.661 + \item measure functions, 47, 112
2.662 + \item \isa {measure_def} (theorem), \bold{113}
2.663 + \item meta-logic, \bold{78}
2.664 \item methods, \bold{16}
2.665 - \item \isa {min} (constant), \hyperpage{23, 24}
2.666 + \item \isa {min} (constant), 23, 24
2.667 \item mixfix annotations, \bold{53}
2.668 - \item \isa {mod} (symbol), \hyperpage{23}
2.669 - \item \isa {mod_div_equality} (theorem), \bold{145}
2.670 - \item \isa {mod_mult_distrib} (theorem), \bold{145}
2.671 - \item model checking example, \hyperpage{110--120}
2.672 - \item \emph{modus ponens}, \hyperpage{61}, \hyperpage{66}
2.673 - \item \isa {mono_def} (theorem), \bold{110}
2.674 - \item monotone functions, \bold{110}, \hyperpage{133}
2.675 - \subitem and inductive definitions, \hyperpage{131--132}
2.676 - \item \isa {more} (constant), \hyperpage{152}, \hyperpage{154}
2.677 - \item \isa {mp} (theorem), \bold{66}
2.678 - \item \isa {mult_ac} (theorems), \hyperpage{146}
2.679 - \item multiple inheritance, \bold{163}
2.680 - \item multiset ordering, \bold{109}
2.681 + \item \isa {mod} (symbol), 23
2.682 + \item \isa {mod_div_equality} (theorem), \bold{149}
2.683 + \item \isa {mod_mult_distrib} (theorem), \bold{149}
2.684 + \item model checking example, 114--124
2.685 + \item \emph{modus ponens}, 65, 70
2.686 + \item \isa {mono_def} (theorem), \bold{114}
2.687 + \item monotone functions, \bold{114}, 137
2.688 + \subitem and inductive definitions, 135--136
2.689 + \item \isa {more} (constant), 156, 158
2.690 + \item \isa {mp} (theorem), \bold{70}
2.691 + \item \isa {mult_ac} (theorems), 150
2.692 + \item multiple inheritance, \bold{167}
2.693 + \item multiset ordering, \bold{113}
2.694
2.695 \indexspace
2.696
2.697 - \item \isa {nat} (type), \hyperpage{4}, \hyperpage{22},
2.698 - \hyperpage{145--147}
2.699 - \item \isa {nat_less_induct} (theorem), \hyperpage{182}
2.700 - \item natural deduction, \hyperpage{61--62}
2.701 - \item natural numbers, \hyperpage{22}, \hyperpage{145--147}
2.702 - \item Needham-Schroeder protocol, \hyperpage{189--191}
2.703 - \item negation, \hyperpage{67--69}
2.704 - \item \isa {Nil} (constant), \hyperpage{9}
2.705 - \item \isa {no_asm} (modifier), \hyperpage{29}
2.706 - \item \isa {no_asm_simp} (modifier), \hyperpage{30}
2.707 - \item \isa {no_asm_use} (modifier), \hyperpage{30}
2.708 - \item non-standard reals, \hyperpage{149}
2.709 + \item \isa {nat} (type), 4, 22, 149--151
2.710 + \item \isa {nat_less_induct} (theorem), 186
2.711 + \item natural deduction, 65--66
2.712 + \item natural numbers, 22, 149--151
2.713 + \item Needham-Schroeder protocol, 193--195
2.714 + \item negation, 71--73
2.715 + \item \isa {Nil} (constant), 9
2.716 + \item \isa {no_asm} (modifier), 29
2.717 + \item \isa {no_asm_simp} (modifier), 30
2.718 + \item \isa {no_asm_use} (modifier), 30
2.719 + \item non-standard reals, 153
2.720 \item \isa {None} (constant), \bold{24}
2.721 - \item \isa {notE} (theorem), \bold{67}
2.722 - \item \isa {notI} (theorem), \bold{67}
2.723 - \item numbers, \hyperpage{143--149}
2.724 - \item numeric literals, \hyperpage{144}
2.725 - \subitem for type \protect\isa{nat}, \hyperpage{145}
2.726 - \subitem for type \protect\isa{real}, \hyperpage{149}
2.727 + \item \isa {notE} (theorem), \bold{71}
2.728 + \item \isa {notI} (theorem), \bold{71}
2.729 + \item numbers, 147--153
2.730 + \item numeric literals, 148
2.731 + \subitem for type \protect\isa{nat}, 149
2.732 + \subitem for type \protect\isa{real}, 153
2.733
2.734 \indexspace
2.735
2.736 - \item \isa {O} (symbol), \hyperpage{106}
2.737 - \item \texttt {o}, \bold{203}
2.738 - \item \isa {o_def} (theorem), \bold{104}
2.739 - \item \isa {OF} (attribute), \hyperpage{89--90}
2.740 - \item \isa {of} (attribute), \hyperpage{87}, \hyperpage{90}
2.741 - \item \isa {only} (modifier), \hyperpage{29}
2.742 - \item \isacommand {oops} (command), \hyperpage{13}
2.743 + \item \isa {O} (symbol), 110
2.744 + \item \texttt {o}, \bold{207}
2.745 + \item \isa {o_def} (theorem), \bold{108}
2.746 + \item \isa {OF} (attribute), 93--94
2.747 + \item \isa {of} (attribute), 91, 94
2.748 + \item \isa {only} (modifier), 29
2.749 + \item \isacommand {oops} (command), 13
2.750 \item \isa {option} (type), \bold{24}
2.751 - \item ordered rewriting, \bold{170}
2.752 - \item overloading, \hyperpage{23}, \hyperpage{159--161}
2.753 - \subitem and arithmetic, \hyperpage{144}
2.754 + \item ordered rewriting, \bold{174}
2.755 + \item overloading, 23, 163--165
2.756 + \subitem and arithmetic, 148
2.757
2.758 \indexspace
2.759
2.760 - \item pairs and tuples, \hyperpage{24}, \hyperpage{149--152}
2.761 + \item pairs and tuples, 24, 153--156
2.762 \item parent theories, \bold{4}
2.763 \item pattern matching
2.764 - \subitem and \isacommand{recdef}, \hyperpage{47}
2.765 + \subitem and \isacommand{recdef}, 47
2.766 \item patterns
2.767 - \subitem higher-order, \bold{171}
2.768 - \item PDL, \hyperpage{112--114}
2.769 - \item \isacommand {pr} (command), \hyperpage{16}, \hyperpage{94}
2.770 - \item \isacommand {prefer} (command), \hyperpage{16}, \hyperpage{94}
2.771 - \item prefix annotation, \bold{56}
2.772 + \subitem higher-order, \bold{175}
2.773 + \item PDL, 116--118
2.774 + \item \isacommand {pr} (command), 16, 98
2.775 + \item \isacommand {prefer} (command), 16, 98
2.776 + \item prefix annotation, 56
2.777 \item primitive recursion, \see{recursion, primitive}{1}
2.778 - \item \isacommand {primrec} (command), \hyperpage{10}, \hyperpage{18},
2.779 - \hyperpage{38--43}
2.780 - \item print mode, \hyperpage{55}
2.781 - \item \isacommand {print\_syntax} (command), \hyperpage{54}
2.782 + \item \isacommand {primrec} (command), 10, 18, 38--43
2.783 + \item print mode, \bold{55}
2.784 + \item \isacommand {print\_syntax} (command), 54
2.785 \item product type, \see{pairs and tuples}{1}
2.786 \item Proof General, \bold{7}
2.787 - \item proof state, \hyperpage{12}
2.788 + \item proof state, 12
2.789 \item proofs
2.790 \subitem abandoning, \bold{13}
2.791 - \subitem examples of failing, \hyperpage{81--83}
2.792 + \subitem examples of failing, 85--87
2.793 \item protocols
2.794 - \subitem security, \hyperpage{189--199}
2.795 + \subitem security, 193--203
2.796
2.797 \indexspace
2.798
2.799 - \item quantifiers, \hyperpage{6}
2.800 - \subitem and inductive definitions, \hyperpage{129--131}
2.801 - \subitem existential, \hyperpage{76}
2.802 - \subitem for sets, \hyperpage{102}
2.803 - \subitem instantiating, \hyperpage{78}
2.804 - \subitem universal, \hyperpage{73--76}
2.805 + \item quantifiers, 6
2.806 + \subitem and inductive definitions, 133--135
2.807 + \subitem existential, 80
2.808 + \subitem for sets, 106
2.809 + \subitem instantiating, 82
2.810 + \subitem universal, 77--80
2.811
2.812 \indexspace
2.813
2.814 - \item \isa {r_into_rtrancl} (theorem), \bold{106}
2.815 - \item \isa {r_into_trancl} (theorem), \bold{107}
2.816 + \item \isa {r_into_rtrancl} (theorem), \bold{110}
2.817 + \item \isa {r_into_trancl} (theorem), \bold{111}
2.818 \item range
2.819 - \subitem of a function, \hyperpage{105}
2.820 - \subitem of a relation, \hyperpage{106}
2.821 - \item \isa {range} (symbol), \hyperpage{105}
2.822 - \item \isa {Range_iff} (theorem), \bold{106}
2.823 - \item \isa {Real} (theory), \hyperpage{149}
2.824 - \item \isa {real} (type), \hyperpage{148--149}
2.825 - \item real numbers, \hyperpage{148--149}
2.826 - \item \isacommand {recdef} (command), \hyperpage{46--52},
2.827 - \hyperpage{108}, \hyperpage{172--180}
2.828 - \subitem and numeric literals, \hyperpage{144}
2.829 - \item \isa {recdef_cong} (attribute), \hyperpage{176}
2.830 - \item \isa {recdef_simp} (attribute), \hyperpage{49}
2.831 - \item \isa {recdef_wf} (attribute), \hyperpage{174}
2.832 - \item \isacommand {record} (command), \hyperpage{153}
2.833 - \item records, \hyperpage{152--158}
2.834 - \subitem extensible, \hyperpage{154--155}
2.835 + \subitem of a function, 109
2.836 + \subitem of a relation, 110
2.837 + \item \isa {range} (symbol), 109
2.838 + \item \isa {Range_iff} (theorem), \bold{110}
2.839 + \item \isa {Real} (theory), 153
2.840 + \item \isa {real} (type), 152--153
2.841 + \item real numbers, 152--153
2.842 + \item \isacommand {recdef} (command), 46--52, 112, 176--184
2.843 + \subitem and numeric literals, 148
2.844 + \item \isa {recdef_cong} (attribute), 180
2.845 + \item \isa {recdef_simp} (attribute), 49
2.846 + \item \isa {recdef_wf} (attribute), 178
2.847 + \item \isacommand {record} (command), 157
2.848 + \item records, 156--162
2.849 + \subitem extensible, 158--159
2.850 \item recursion
2.851 - \subitem guarded, \hyperpage{177}
2.852 - \subitem primitive, \hyperpage{18}
2.853 - \subitem well-founded, \bold{173}
2.854 - \item recursion induction, \hyperpage{51--52}
2.855 - \item \isacommand {redo} (command), \hyperpage{16}
2.856 - \item reflexive and transitive closure, \hyperpage{106--108}
2.857 + \subitem guarded, 181
2.858 + \subitem primitive, 18
2.859 + \subitem well-founded, \bold{177}
2.860 + \item recursion induction, 51--52
2.861 + \item \isacommand {redo} (command), 16
2.862 + \item reflexive and transitive closure, 110--112
2.863 \item reflexive transitive closure
2.864 - \subitem defining inductively, \hyperpage{126--129}
2.865 - \item \isa {rel_comp_def} (theorem), \bold{106}
2.866 - \item relations, \hyperpage{105--108}
2.867 - \subitem well-founded, \hyperpage{108--109}
2.868 - \item \isa {rename_tac} (method), \hyperpage{76--77}
2.869 - \item \isa {rev} (constant), \hyperpage{10--14}, \hyperpage{34}
2.870 + \subitem defining inductively, 130--133
2.871 + \item \isa {rel_comp_def} (theorem), \bold{110}
2.872 + \item relations, 109--112
2.873 + \subitem well-founded, 112--113
2.874 + \item \isa {rename_tac} (method), 80--81
2.875 + \item \isa {rev} (constant), 10--14, 34
2.876 \item rewrite rules, \bold{27}
2.877 - \subitem permutative, \bold{170}
2.878 + \subitem permutative, \bold{174}
2.879 \item rewriting, \bold{27}
2.880 - \item \isa {rotate_tac} (method), \hyperpage{30}
2.881 - \item \isa {rtrancl_refl} (theorem), \bold{106}
2.882 - \item \isa {rtrancl_trans} (theorem), \bold{106}
2.883 - \item rule induction, \hyperpage{122--124}
2.884 - \item rule inversion, \hyperpage{124--125}, \hyperpage{133--134}
2.885 - \item \isa {rule_format} (attribute), \hyperpage{181}
2.886 - \item \isa {rule_tac} (method), \hyperpage{70}
2.887 - \subitem and renaming, \hyperpage{77}
2.888 + \item \isa {rotate_tac} (method), 30
2.889 + \item \isa {rtrancl_refl} (theorem), \bold{110}
2.890 + \item \isa {rtrancl_trans} (theorem), \bold{110}
2.891 + \item rule induction, 126--128
2.892 + \item rule inversion, 128--129, 137--138
2.893 + \item \isa {rule_format} (attribute), 185
2.894 + \item \isa {rule_tac} (method), 74
2.895 + \subitem and renaming, 81
2.896
2.897 \indexspace
2.898
2.899 - \item \isa {safe} (method), \hyperpage{85, 86}
2.900 - \item safe rules, \bold{84}
2.901 + \item \isa {safe} (method), 89, 90
2.902 + \item safe rules, \bold{88}
2.903 + \item \isacommand {sect} (command), 59
2.904 + \item \isacommand {section} (command), 59
2.905 \item selector
2.906 - \subitem record, \hyperpage{153}
2.907 - \item \isa {set} (type), \hyperpage{5}, \hyperpage{99}
2.908 - \item set comprehensions, \hyperpage{101--102}
2.909 - \item \isa {set_ext} (theorem), \bold{100}
2.910 - \item sets, \hyperpage{99--103}
2.911 - \subitem finite, \hyperpage{103}
2.912 - \subitem notation for finite, \bold{101}
2.913 + \subitem record, 157
2.914 + \item session, \bold{58}
2.915 + \item \isa {set} (type), 5, 103
2.916 + \item set comprehensions, 105--106
2.917 + \item \isa {set_ext} (theorem), \bold{104}
2.918 + \item sets, 103--107
2.919 + \subitem finite, 107
2.920 + \subitem notation for finite, \bold{105}
2.921 \item settings, \see{flags}{1}
2.922 - \item \isa {show_brackets} (flag), \hyperpage{6}
2.923 - \item \isa {show_types} (flag), \hyperpage{5}, \hyperpage{16}
2.924 - \item \isa {simp} (attribute), \hyperpage{11}, \hyperpage{28}
2.925 + \item \isa {show_brackets} (flag), 6
2.926 + \item \isa {show_types} (flag), 5, 16
2.927 + \item \isa {simp} (attribute), 11, 28
2.928 \item \isa {simp} (method), \bold{28}
2.929 - \item \isa {simp} del (attribute), \hyperpage{28}
2.930 - \item \isa {simp_all} (method), \hyperpage{29}, \hyperpage{38}
2.931 - \item simplification, \hyperpage{27--33}, \hyperpage{169--172}
2.932 - \subitem of \isa{let}-expressions, \hyperpage{31}
2.933 - \subitem with definitions, \hyperpage{30}
2.934 - \subitem with/of assumptions, \hyperpage{29}
2.935 - \item simplification rule, \hyperpage{171--172}
2.936 - \item simplification rules, \hyperpage{28}
2.937 - \subitem adding and deleting, \hyperpage{29}
2.938 - \item \isa {simplified} (attribute), \hyperpage{87}, \hyperpage{90}
2.939 - \item \isa {size} (constant), \hyperpage{17}
2.940 - \item \isa {snd} (constant), \hyperpage{24}
2.941 - \item \isa {SOME} (symbol), \hyperpage{80}
2.942 - \item \texttt {SOME}, \bold{203}
2.943 + \item \isa {simp} del (attribute), 28
2.944 + \item \isa {simp_all} (method), 29, 38
2.945 + \item simplification, 27--33, 173--176
2.946 + \subitem of \isa{let}-expressions, 31
2.947 + \subitem with definitions, 30
2.948 + \subitem with/of assumptions, 29
2.949 + \item simplification rule, 175--176
2.950 + \item simplification rules, 28
2.951 + \subitem adding and deleting, 29
2.952 + \item \isa {simplified} (attribute), 91, 94
2.953 + \item \isa {size} (constant), 17
2.954 + \item \isa {snd} (constant), 24
2.955 + \item \isa {SOME} (symbol), 84
2.956 + \item \texttt {SOME}, \bold{207}
2.957 \item \isa {Some} (constant), \bold{24}
2.958 - \item \isa {some_equality} (theorem), \bold{80}
2.959 - \item \isa {someI} (theorem), \bold{80}
2.960 - \item \isa {someI2} (theorem), \bold{80}
2.961 - \item \isa {someI_ex} (theorem), \bold{81}
2.962 - \item sorts, \hyperpage{164}
2.963 - \item \isa {spec} (theorem), \bold{74}
2.964 - \item \isa {split} (attribute), \hyperpage{32}
2.965 - \item \isa {split} (constant), \hyperpage{150}
2.966 - \item \isa {split} (method), \hyperpage{31}, \hyperpage{150}
2.967 - \item \isa {split} (modifier), \hyperpage{32}
2.968 + \item \isa {some_equality} (theorem), \bold{84}
2.969 + \item \isa {someI} (theorem), \bold{84}
2.970 + \item \isa {someI2} (theorem), \bold{84}
2.971 + \item \isa {someI_ex} (theorem), \bold{85}
2.972 + \item sorts, 168
2.973 + \item \isa {spec} (theorem), \bold{78}
2.974 + \item \isa {split} (attribute), 32
2.975 + \item \isa {split} (constant), 154
2.976 + \item \isa {split} (method), 31, 154
2.977 + \item \isa {split} (modifier), 32
2.978 \item split rule, \bold{32}
2.979 - \item \isa {split_if} (theorem), \hyperpage{32}
2.980 - \item \isa {split_if_asm} (theorem), \hyperpage{32}
2.981 - \item \isa {ssubst} (theorem), \bold{71}
2.982 + \item \isa {split_if} (theorem), 32
2.983 + \item \isa {split_if_asm} (theorem), 32
2.984 + \item \isa {ssubst} (theorem), \bold{75}
2.985 \item structural induction, \see{induction, structural}{1}
2.986 - \item subclasses, \hyperpage{158}, \hyperpage{163}
2.987 - \item subgoal numbering, \hyperpage{46}
2.988 - \item \isa {subgoal_tac} (method), \hyperpage{92}
2.989 - \item subgoals, \hyperpage{12}
2.990 - \item subset relation, \bold{100}
2.991 - \item \isa {subsetD} (theorem), \bold{100}
2.992 - \item \isa {subsetI} (theorem), \bold{100}
2.993 - \item \isa {subst} (method), \hyperpage{71}
2.994 - \item substitution, \hyperpage{71--73}
2.995 - \item \isa {Suc} (constant), \hyperpage{22}
2.996 - \item \isa {surj_def} (theorem), \bold{104}
2.997 - \item surjections, \hyperpage{104}
2.998 - \item \isa {sym} (theorem), \bold{88}
2.999 + \item subclasses, 162, 167
2.1000 + \item subgoal numbering, 46
2.1001 + \item \isa {subgoal_tac} (method), 96
2.1002 + \item subgoals, 12
2.1003 + \item \isacommand {subsect} (command), 59
2.1004 + \item \isacommand {subsection} (command), 59
2.1005 + \item subset relation, \bold{104}
2.1006 + \item \isa {subsetD} (theorem), \bold{104}
2.1007 + \item \isa {subsetI} (theorem), \bold{104}
2.1008 + \item \isa {subst} (method), 75
2.1009 + \item substitution, 75--77
2.1010 + \item \isacommand {subsubsect} (command), 59
2.1011 + \item \isacommand {subsubsection} (command), 59
2.1012 + \item \isa {Suc} (constant), 22
2.1013 + \item \isa {surj_def} (theorem), \bold{108}
2.1014 + \item surjections, 108
2.1015 + \item \isa {sym} (theorem), \bold{92}
2.1016 \item symbols, \bold{55}
2.1017 - \item syntax, \hyperpage{6}, \hyperpage{11}
2.1018 - \item \isacommand {syntax} (command), \hyperpage{56}
2.1019 - \item syntax translations, \hyperpage{57}
2.1020 + \item syntax, 6, 11
2.1021 + \item \isacommand {syntax} (command), 56
2.1022 + \item syntax translations, 57
2.1023
2.1024 \indexspace
2.1025
2.1026 - \item tacticals, \hyperpage{93}
2.1027 - \item tactics, \hyperpage{12}
2.1028 - \item \isacommand {term} (command), \hyperpage{16}
2.1029 + \item tacticals, 97
2.1030 + \item tactics, 12
2.1031 + \item \isacommand {term} (command), 16
2.1032 \item term rewriting, \bold{27}
2.1033 \item termination, \see{functions, total}{1}
2.1034 - \item terms, \hyperpage{5}
2.1035 - \item \isa {THE} (symbol), \hyperpage{79}
2.1036 - \item \isa {the_equality} (theorem), \bold{79}
2.1037 - \item \isa {THEN} (attribute), \bold{88}, \hyperpage{90},
2.1038 - \hyperpage{96}
2.1039 - \item \isacommand {theorem} (command), \bold{11}, \hyperpage{13}
2.1040 - \item theories, \hyperpage{4}
2.1041 + \item terms, 5
2.1042 + \item \isa {THE} (symbol), 83
2.1043 + \item \isa {the_equality} (theorem), \bold{83}
2.1044 + \item \isa {THEN} (attribute), \bold{92}, 94, 100
2.1045 + \item \isacommand {theorem} (command), \bold{11}, 13
2.1046 + \item theories, 4
2.1047 \subitem abandoning, \bold{16}
2.1048 - \item \isacommand {theory} (command), \hyperpage{16}
2.1049 - \item theory files, \hyperpage{4}
2.1050 - \item \isacommand {thm} (command), \hyperpage{16}
2.1051 - \item \isa {tl} (constant), \hyperpage{17}
2.1052 - \item \isa {ToyList} example, \hyperpage{9--14}
2.1053 - \item \isa {trace_simp} (flag), \hyperpage{33}
2.1054 + \item \isacommand {theory} (command), 16
2.1055 + \item theory files, 4
2.1056 + \item \isacommand {thm} (command), 16
2.1057 + \item \isa {tl} (constant), 17
2.1058 + \item \isa {ToyList} example, 9--14
2.1059 + \item \isa {trace_simp} (flag), 33
2.1060 \item tracing the simplifier, \bold{33}
2.1061 - \item \isa {trancl_trans} (theorem), \bold{107}
2.1062 - \item transition systems, \hyperpage{111}
2.1063 - \item \isacommand {translations} (command), \hyperpage{57}
2.1064 - \item tries, \hyperpage{44--46}
2.1065 - \item \isa {True} (constant), \hyperpage{5}
2.1066 - \item \isa {truncate} (constant), \hyperpage{157}
2.1067 + \item \isa {trancl_trans} (theorem), \bold{111}
2.1068 + \item transition systems, 115
2.1069 + \item \isacommand {translations} (command), 57
2.1070 + \item tries, 44--46
2.1071 + \item \isa {True} (constant), 5
2.1072 + \item \isa {truncate} (constant), 161
2.1073 \item tuples, \see{pairs and tuples}{1}
2.1074 - \item \isacommand {typ} (command), \hyperpage{16}
2.1075 + \item \isacommand {typ} (command), 16
2.1076 \item type constraints, \bold{6}
2.1077 - \item type constructors, \hyperpage{5}
2.1078 + \item type constructors, 5
2.1079 \item type inference, \bold{5}
2.1080 - \item type synonyms, \hyperpage{25}
2.1081 - \item type variables, \hyperpage{5}
2.1082 - \item \isacommand {typedecl} (command), \hyperpage{111},
2.1083 - \hyperpage{165}
2.1084 - \item \isacommand {typedef} (command), \hyperpage{165--168}
2.1085 - \item types, \hyperpage{4--5}
2.1086 - \subitem declaring, \hyperpage{165}
2.1087 - \subitem defining, \hyperpage{165--168}
2.1088 - \item \isacommand {types} (command), \hyperpage{25}
2.1089 + \item type synonyms, 25
2.1090 + \item type variables, 5
2.1091 + \item \isacommand {typedecl} (command), 115, 169
2.1092 + \item \isacommand {typedef} (command), 169--172
2.1093 + \item types, 4--5
2.1094 + \subitem declaring, 169
2.1095 + \subitem defining, 169--172
2.1096 + \item \isacommand {types} (command), 25
2.1097
2.1098 \indexspace
2.1099
2.1100 - \item Ullman, J. D., \hyperpage{139}
2.1101 - \item \texttt {UN}, \bold{203}
2.1102 - \item \texttt {Un}, \bold{203}
2.1103 - \item \isa {UN_E} (theorem), \bold{102}
2.1104 - \item \isa {UN_I} (theorem), \bold{102}
2.1105 - \item \isa {UN_iff} (theorem), \bold{102}
2.1106 - \item \isa {Un_subset_iff} (theorem), \bold{100}
2.1107 - \item \isacommand {undo} (command), \hyperpage{16}
2.1108 + \item Ullman, J. D., 143
2.1109 + \item \texttt {UN}, \bold{207}
2.1110 + \item \texttt {Un}, \bold{207}
2.1111 + \item \isa {UN_E} (theorem), \bold{106}
2.1112 + \item \isa {UN_I} (theorem), \bold{106}
2.1113 + \item \isa {UN_iff} (theorem), \bold{106}
2.1114 + \item \isa {Un_subset_iff} (theorem), \bold{104}
2.1115 + \item \isacommand {undo} (command), 16
2.1116 \item \isa {unfold} (method), \bold{31}
2.1117 - \item Unicode, \hyperpage{55}
2.1118 - \item unification, \hyperpage{70--73}
2.1119 - \item \isa {UNION} (constant), \hyperpage{103}
2.1120 - \item \texttt {Union}, \bold{203}
2.1121 + \item Unicode, 55
2.1122 + \item unification, 74--77
2.1123 + \item \isa {UNION} (constant), 107
2.1124 + \item \texttt {Union}, \bold{207}
2.1125 \item union
2.1126 - \subitem indexed, \hyperpage{102}
2.1127 - \item \isa {Union_iff} (theorem), \bold{102}
2.1128 - \item \isa {unit} (type), \hyperpage{24}
2.1129 - \item unknowns, \hyperpage{7}, \bold{62}
2.1130 - \item unsafe rules, \bold{84}
2.1131 + \subitem indexed, 106
2.1132 + \item \isa {Union_iff} (theorem), \bold{106}
2.1133 + \item \isa {unit} (type), 24
2.1134 + \item unknowns, 7, \bold{66}
2.1135 + \item unsafe rules, \bold{88}
2.1136 \item update
2.1137 - \subitem record, \hyperpage{153}
2.1138 - \item updating a function, \bold{103}
2.1139 + \subitem record, 157
2.1140 + \item updating a function, \bold{107}
2.1141
2.1142 \indexspace
2.1143
2.1144 - \item variables, \hyperpage{7}
2.1145 - \subitem schematic, \hyperpage{7}
2.1146 - \subitem type, \hyperpage{5}
2.1147 - \item \isa {vimage_def} (theorem), \bold{105}
2.1148 + \item variables, 7
2.1149 + \subitem schematic, 7
2.1150 + \subitem type, 5
2.1151 + \item \isa {vimage_def} (theorem), \bold{109}
2.1152
2.1153 \indexspace
2.1154
2.1155 - \item Wenzel, Markus, \hyperpage{vii}
2.1156 - \item \isa {wf_induct} (theorem), \bold{109}
2.1157 - \item \isa {wf_inv_image} (theorem), \bold{109}
2.1158 - \item \isa {wf_less_than} (theorem), \bold{108}
2.1159 - \item \isa {wf_lex_prod} (theorem), \bold{109}
2.1160 - \item \isa {wf_measure} (theorem), \bold{109}
2.1161 - \item \isa {wf_subset} (theorem), \hyperpage{174}
2.1162 - \item \isa {while} (constant), \hyperpage{179}
2.1163 - \item \isa {While_Combinator} (theory), \hyperpage{179}
2.1164 - \item \isa {while_rule} (theorem), \hyperpage{179}
2.1165 + \item Wenzel, Markus, vii
2.1166 + \item \isa {wf_induct} (theorem), \bold{113}
2.1167 + \item \isa {wf_inv_image} (theorem), \bold{113}
2.1168 + \item \isa {wf_less_than} (theorem), \bold{112}
2.1169 + \item \isa {wf_lex_prod} (theorem), \bold{113}
2.1170 + \item \isa {wf_measure} (theorem), \bold{113}
2.1171 + \item \isa {wf_subset} (theorem), 178
2.1172 + \item \isa {while} (constant), 183
2.1173 + \item \isa {While_Combinator} (theory), 183
2.1174 + \item \isa {while_rule} (theorem), 183
2.1175
2.1176 \indexspace
2.1177
2.1178 - \item \isa {zadd_ac} (theorems), \hyperpage{147}
2.1179 - \item \isa {zmult_ac} (theorems), \hyperpage{147}
2.1180 + \item \isa {zadd_ac} (theorems), 151
2.1181 + \item \isa {zmult_ac} (theorems), 151
2.1182
2.1183 \end{theindex}