
diff -r 0c86acc069ad -r 5deda0549f97 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Thu Jul 26 16:54:44 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,933 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Documents}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The core concept of Isabelle's framework for concrete syntax is that
-  of \bfindex{mixfix annotations}.  Associated with any kind of
-  constant declaration, mixfixes affect both the grammar productions
-  for the parser and output templates for the pretty printer.
-
-  In full generality, parser and pretty printer configuration is a
-  subtle affair~\cite{isabelle-ref}.  Your syntax specifications need
-  to interact properly with the existing setup of Isabelle/Pure and
-  Isabelle/HOL\@.  To avoid creating ambiguities with existing
-  elements, it is particularly important to give new syntactic
-  constructs the right precedence.
-
-  Below we introduce a few simple syntax declaration
-  forms that already cover many common situations fairly well.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Infix Annotations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Syntax annotations may be included wherever constants are declared,
-  such as \isacommand{definition} and \isacommand{primrec} --- and also
-  \isacommand{datatype}, which declares constructor operations.
-  Type-constructors may be annotated as well, although this is less
-  frequently encountered in practice (the infix type \isa{{\isaliteral{5C3C74696D65733E}{\isasymtimes}}} comes
-  to mind).
-
-  Infix declarations\index{infix annotations} provide a useful special
-  case of mixfixes.  The following example of the exclusive-or
-  operation on boolean values illustrates typical infix declarations.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{definition}\isamarkupfalse%
-\ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent Now \isa{xor\ A\ B} and \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B} refer to the
-  same expression internally.  Any curried function with at least two
-  arguments may be given infix syntax.  For partial applications with
-  fewer than two operands, there is a notation using the prefix~\isa{op}.  For instance, \isa{xor} without arguments is represented as
-  \isa{op\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}}; together with ordinary function application, this
-  turns \isa{xor\ A} into \isa{op\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ A}.
-
-  The keyword \isakeyword{infixl} seen above specifies an
-  infix operator that is nested to the \emph{left}: in iterated
-  applications the more complex expression appears on the left-hand
-  side, and \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} stands for \isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C}.  Similarly, \isakeyword{infixr} means nesting to the
-  \emph{right}, reading \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} as \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C{\isaliteral{29}{\isacharparenright}}}.  A \emph{non-oriented} declaration via \isakeyword{infix}
-  would render \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} illegal, but demand explicit
-  parentheses to indicate the intended grouping.
-
-  The string \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} in our annotation refers to the
-  concrete syntax to represent the operator (a literal token), while
-  the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct:
-  the syntactic priorities of the arguments and result.  Isabelle/HOL
-  already uses up many popular combinations of ASCII symbols for its
-  own use, including both \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}}.  Longer
-  character combinations are more likely to be still available for
-  user extensions, such as our~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}}.
-
-  Operator precedences have a range of 0--1000.  Very low or high
-  priorities are reserved for the meta-logic.  HOL syntax mainly uses
-  the range of 10--100: the equality infix \isa{{\isaliteral{3D}{\isacharequal}}} is centered at
-  50; logical connectives (like \isa{{\isaliteral{5C3C6F723E}{\isasymor}}} and \isa{{\isaliteral{5C3C616E643E}{\isasymand}}}) are
-  below 50; algebraic ones (like \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}}) are
-  above 50.  User syntax should strive to coexist with common HOL
-  forms, or use the mostly unused range 100--900.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Concrete syntax based on ASCII characters has inherent limitations.
-  Mathematical notation demands a larger repertoire of glyphs.
-  Several standards of extended character sets have been proposed over
-  decades, but none has become universally available so far.  Isabelle
-  has its own notion of \bfindex{symbols} as the smallest entities of
-  source text, without referring to internal encodings.  There are
-  three kinds of such ``generalized characters'':
-
-  \begin{enumerate}
-
-  \item 7-bit ASCII characters
-
-  \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
-
-  \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
-
-  \end{enumerate}
-
-  Here $ident$ is any sequence of letters. 
-  This results in an infinite store of symbols, whose
-  interpretation is left to further front-end tools.  For example, the
-  user-interface of Proof~General + X-Symbol and the Isabelle document
-  processor (see \S\ref{sec:document-preparation}) display the
-  \verb,\,\verb,<forall>, symbol as~\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}.
-
-  A list of standard Isabelle symbols is given in
-  \cite{isabelle-isar-ref}.  You may introduce your own
-  interpretation of further symbols by configuring the appropriate
-  front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
-  macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
-  few predefined control symbols, such as \verb,\,\verb,<^sub>, and
-  \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
-  printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
-  output as \isa{A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{5C3C737461723E}{\isasymstar}}}.
-
-  A number of symbols are considered letters by the Isabelle lexer and
-  can be used as part of identifiers. These are the greek letters
-  \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} (\verb+\+\verb+<alpha>+), \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}
-  (\verb+\+\verb+<beta>+), etc. (excluding \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}),
-  special letters like \isa{{\isaliteral{5C3C413E}{\isasymA}}} (\verb+\+\verb+<A>+) and \isa{{\isaliteral{5C3C41413E}{\isasymAA}}} (\verb+\+\verb+<AA>+), and the control symbols
-  \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
-  sub and super scripts. This means that the input
-
-  \medskip
-  {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
-
-  \medskip
-  \noindent is recognized as the term \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C50693E}{\isasymPi}}\isaliteral{5C3C5E697375703E}{}\isactrlisup {\isaliteral{5C3C413E}{\isasymA}}} 
-  by Isabelle. Note that \isa{{\isaliteral{5C3C50693E}{\isasymPi}}\isaliteral{5C3C5E697375703E}{}\isactrlisup {\isaliteral{5C3C413E}{\isasymA}}} is a single
-  syntactic entity, not an exponentiation.
-
-  Replacing our previous definition of \isa{xor} by the
-  following specifies an Isabelle symbol for the new operator:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isacommand{definition}\isamarkupfalse%
-\ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\noindent Proof~General provides several input methods to enter
-  \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text.  If all fails one may just type a named
-  entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will
-  be displayed after further input.
-
-  More flexible is to provide alternative syntax forms
-  through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By
-  convention, the mode of ``$xsymbols$'' is enabled whenever
-  Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
-  consider the following hybrid declaration of \isa{xor}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isacommand{definition}\isamarkupfalse%
-\ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{notation}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}\ xor\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\noindent
-The \commdx{notation} command associates a mixfix
-annotation with a known constant.  The print mode specification,
-here \isa{{\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}}, is optional.
-
-We may now write \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B} or \isa{A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B} in input, while
-output uses the nicer syntax of $xsymbols$ whenever that print mode is
-active.  Such an arrangement is particularly useful for interactive
-development, where users may type ASCII text and see mathematical
-symbols displayed during proofs.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Prefix Annotations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Prefix syntax annotations\index{prefix annotation} are another form
-  of mixfixes \cite{isabelle-ref}, without any template arguments or
-  priorities --- just some literal syntax.  The following example
-  associates common symbols with the constructors of a datatype.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{datatype}\isamarkupfalse%
-\ currency\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ Euro\ nat\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6575726F3E}{\isasymeuro}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ Pounds\ nat\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C706F756E64733E}{\isasympounds}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ Yen\ nat\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C79656E3E}{\isasymyen}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ Dollar\ nat\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{24}{\isachardollar}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptext}%
-\noindent Here the mixfix annotations on the rightmost column happen
-  to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
-  \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
-  that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ currency}.  The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
-  printed as \isa{{\isaliteral{5C3C6575726F3E}{\isasymeuro}}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
-  subject to our concrete syntax.  This rather simple form already
-  achieves conformance with notational standards of the European
-  Commission.
-
-  Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Abbreviations \label{sec:abbreviations}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Mixfix syntax annotations merely decorate particular constant
-application forms with concrete syntax, for instance replacing
-\isa{xor\ A\ B} by \isa{A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B}.  Occasionally, the relationship
-between some piece of notation and its internal form is more
-complicated.  Here we need \emph{abbreviations}.
-
-Command \commdx{abbreviation} introduces an uninterpreted notational
-constant as an abbreviation for a complex term. Abbreviations are
-unfolded upon parsing and re-introduced upon printing. This provides a
-simple mechanism for syntactic macros.
-
-A typical use of abbreviations is to introduce relational notation for
-membership in a set of pairs, replacing \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim} by
-\isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}. We assume that a constant \isa{sim} of type
-\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set} has been introduced at this point.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{abbreviation}\isamarkupfalse%
-\ sim{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C617070726F783E}{\isasymapprox}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent The given meta-equality is used as a rewrite rule
-after parsing (replacing \mbox{\isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}} by \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim}) and before printing (turning \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim} back into
-\mbox{\isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}}). The name of the dummy constant \isa{sim{\isadigit{2}}}
-does not matter, as long as it is unique.
-
-Another common application of abbreviations is to
-provide variant versions of fundamental relational expressions, such
-as \isa{{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}} for negated equalities.  The following declaration
-stems from Isabelle/HOL itself:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{abbreviation}\isamarkupfalse%
-\ not{\isaliteral{5F}{\isacharunderscore}}equal\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{7E}{\isachartilde}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}\ y\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{notation}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}\ not{\isaliteral{5F}{\isacharunderscore}}equal\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptext}%
-\noindent The notation \isa{{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}} is introduced separately to restrict it
-to the \emph{xsymbols} mode.
-
-Abbreviations are appropriate when the defined concept is a
-simple variation on an existing one.  But because of the automatic
-folding and unfolding of abbreviations, they do not scale up well to
-large hierarchies of concepts. Abbreviations do not replace
-definitions.
-
-Abbreviations are a simplified form of the general concept of
-\emph{syntax translations}; even heavier transformations may be
-written in ML \cite{isabelle-ref}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Document Preparation \label{sec:document-preparation}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle/Isar is centered around the concept of \bfindex{formal
-  proof documents}\index{documents|bold}.  The outcome of a formal
-  development effort is meant to be a human-readable record, presented
-  as browsable PDF file or printed on paper.  The overall document
-  structure follows traditional mathematical articles, with sections,
-  intermediate explanations, definitions, theorems and proofs.
-
-  \medskip The Isabelle document preparation system essentially acts
-  as a front-end to {\LaTeX}.  After checking specifications and
-  proofs formally, the theory sources are turned into typesetting
-  instructions in a schematic manner.  This lets you write authentic
-  reports on theory developments with little effort: many technical
-  consistency checks are handled by the system.
-
-  Here is an example to illustrate the idea of Isabelle document
-  preparation.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{quotation}
-%
-\begin{isamarkuptext}%
-The following datatype definition of \isa{{\isaliteral{27}{\isacharprime}}a\ bintree} models
-  binary trees with nodes being decorated by elements of type \isa{{\isaliteral{27}{\isacharprime}}a}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{datatype}\isamarkupfalse%
-\ {\isaliteral{27}{\isacharprime}}a\ bintree\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ \ Leaf\ {\isaliteral{7C}{\isacharbar}}\ Branch\ {\isaliteral{27}{\isacharprime}}a\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bintree{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bintree{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent The datatype induction rule generated here is of the form
-  \begin{isabelle}%
-\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ Leaf{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isaindent{\ \ }{\isaliteral{5C3C416E643E}{\isasymAnd}}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isaliteral{2E}{\isachardot}}\isanewline
-\isaindent{\ \ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ bintree{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ bintree{\isadigit{2}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
-\isaindent{\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ bintree%
-\end{isabelle}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\end{quotation}
-%
-\begin{isamarkuptext}%
-\noindent The above document output has been produced as follows:
-
-  \begin{ttbox}
-  text {\ttlbrace}*
-    The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
-    models binary trees with nodes being decorated by elements
-    of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
-  *{\ttrbrace}
-
-  datatype 'a bintree =
-    Leaf | Branch 'a  "'a bintree"  "'a bintree"
-  \end{ttbox}
-  \begin{ttbox}
-  text {\ttlbrace}*
-    {\ttback}noindent The datatype induction rule generated here is
-    of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
-  *{\ttrbrace}
-  \end{ttbox}\vspace{-\medskipamount}
-
-  \noindent Here we have augmented the theory by formal comments
-  (using \isakeyword{text} blocks), the informal parts may again refer
-  to formal entities by means of ``antiquotations'' (such as
-  \texttt{\at}\verb,{text "'a bintree"}, or
-  \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Isabelle Sessions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In contrast to the highly interactive mode of Isabelle/Isar theory
-  development, the document preparation stage essentially works in
-  batch-mode.  An Isabelle \bfindex{session} consists of a collection
-  of source files that may contribute to an output document.  Each
-  session is derived from a single parent, usually an object-logic
-  image like \texttt{HOL}.  This results in an overall tree structure,
-  which is reflected by the output location in the file system
-  (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
-
-  \medskip The easiest way to manage Isabelle sessions is via
-  \texttt{isabelle mkdir} (generates an initial session source setup)
-  and \texttt{isabelle make} (run sessions controlled by
-  \texttt{IsaMakefile}).  For example, a new session
-  \texttt{MySession} derived from \texttt{HOL} may be produced as
-  follows:
-
-\begin{verbatim}
-  isabelle mkdir HOL MySession
-  isabelle make
-\end{verbatim}
-
-  The \texttt{isabelle make} job also informs about the file-system
-  location of the ultimate results.  The above dry run should be able
-  to produce some \texttt{document.pdf} (with dummy title, empty table
-  of contents etc.).  Any failure at this stage usually indicates
-  technical problems of the {\LaTeX} installation.
-
-  \medskip The detailed arrangement of the session sources is as
-  follows.
-
-  \begin{itemize}
-
-  \item Directory \texttt{MySession} holds the required theory files
-  $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
-
-  \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
-  for loading all wanted theories, usually just
-  ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
-  dependency graph.
-
-  \item Directory \texttt{MySession/document} contains everything
-  required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
-  provided initially.
-
-  The latter file holds appropriate {\LaTeX} code to commence a
-  document (\verb,\documentclass, etc.), and to include the generated
-  files $T@i$\texttt{.tex} for each theory.  Isabelle will generate a
-  file \texttt{session.tex} holding {\LaTeX} commands to include all
-  generated theory output files in topologically sorted order, so
-  \verb,\input{session}, in the body of \texttt{root.tex} does the job
-  in most situations.
-
-  \item \texttt{IsaMakefile} holds appropriate dependencies and
-  invocations of Isabelle tools to control the batch job.  In fact,
-  several sessions may be managed by the same \texttt{IsaMakefile}.
-  See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
-  for further details, especially on
-  \texttt{isabelle usedir} and \texttt{isabelle make}.
-
-  \end{itemize}
-
-  One may now start to populate the directory \texttt{MySession}, and
-  the file \texttt{MySession/ROOT.ML} accordingly.  The file
-  \texttt{MySession/document/root.tex} should also be adapted at some
-  point; the default version is mostly self-explanatory.  Note that
-  \verb,\isabellestyle, enables fine-tuning of the general appearance
-  of characters and mathematical symbols (see also
-  \S\ref{sec:doc-prep-symbols}).
-
-  Especially observe the included {\LaTeX} packages \texttt{isabelle}
-  (mandatory), \texttt{isabellesym} (required for mathematical
-  symbols), and the final \texttt{pdfsetup} (provides sane defaults
-  for \texttt{hyperref}, including URL markup).  All three are
-  distributed with Isabelle. Further packages may be required in
-  particular applications, say for unusual mathematical symbols.
-
-  \medskip Any additional files for the {\LaTeX} stage go into the
-  \texttt{MySession/document} directory as well.  In particular,
-  adding a file named \texttt{root.bib} causes an automatic run of
-  \texttt{bibtex} to process a bibliographic database; see also
-  \texttt{isabelle document} \cite{isabelle-sys}.
-
-  \medskip Any failure of the document preparation phase in an
-  Isabelle batch session leaves the generated sources in their target
-  location, identified by the accompanying error message.  This lets
-  you trace {\LaTeX} problems with the generated files at hand.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Structure Markup%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The large-scale structure of Isabelle documents follows existing
-  {\LaTeX} conventions, with chapters, sections, subsubsections etc.
-  The Isar language includes separate \bfindex{markup commands}, which
-  do not affect the formal meaning of a theory (or proof), but result
-  in corresponding {\LaTeX} elements.
-
-  There are separate markup commands depending on the textual context:
-  in header position (just before \isakeyword{theory}), within the
-  theory body, or within a proof.  The header needs to be treated
-  specially here, since ordinary theory and proof commands may only
-  occur \emph{after} the initial \isakeyword{theory} specification.
-
-  \medskip
-
-  \begin{tabular}{llll}
-  header & theory & proof & default meaning \\\hline
-    & \commdx{chapter} & & \verb,\chapter, \\
-  \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
-    & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
-    & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
-  \end{tabular}
-
-  \medskip
-
-  From the Isabelle perspective, each markup command takes a single
-  $text$ argument (delimited by \verb,",~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,", or
-  \verb,{,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,},).  After stripping any
-  surrounding white space, the argument is passed to a {\LaTeX} macro
-  \verb,\isamarkupXYZ, for command \isakeyword{XYZ}.  These macros are
-  defined in \verb,isabelle.sty, according to the meaning given in the
-  rightmost column above.
-
-  \medskip The following source fragment illustrates structure markup
-  of a theory.  Note that {\LaTeX} labels may be included inside of
-  section headings as well.
-
-  \begin{ttbox}
-  header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
-
-  theory Foo_Bar
-  imports Main
-  begin
-
-  subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
-
-  definition foo :: \dots
-
-  definition bar :: \dots
-
-  subsection {\ttlbrace}* Derived rules *{\ttrbrace}
-
-  lemma fooI: \dots
-  lemma fooE: \dots
-
-  subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
-
-  theorem main: \dots
-
-  end
-  \end{ttbox}\vspace{-\medskipamount}
-
-  You may occasionally want to change the meaning of markup commands,
-  say via \verb,\renewcommand, in \texttt{root.tex}.  For example,
-  \verb,\isamarkupheader, is a good candidate for some tuning.  We
-  could move it up in the hierarchy to become \verb,\chapter,.
-
-\begin{verbatim}
-  \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
-\end{verbatim}
-
-  \noindent Now we must change the document class given in
-  \texttt{root.tex} to something that supports chapters.  A suitable
-  command is \verb,\documentclass{report},.
-
-  \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
-  hold the name of the current theory context.  This is particularly
-  useful for document headings:
-
-\begin{verbatim}
-  \renewcommand{\isamarkupheader}[1]
-  {\chapter{#1}\markright{THEORY~\isabellecontext}}
-\end{verbatim}
-
-  \noindent Make sure to include something like
-  \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
-  should have more than two pages to show the effect.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle \bfindex{source comments}, which are of the form
-  \verb,(,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,),, essentially act like
-  white space and do not really contribute to the content.  They
-  mainly serve technical purposes to mark certain oddities in the raw
-  input text.  In contrast, \bfindex{formal comments} are portions of
-  text that are associated with formal Isabelle/Isar commands
-  (\bfindex{marginal comments}), or as standalone paragraphs within a
-  theory or proof context (\bfindex{text blocks}).
-
-  \medskip Marginal comments are part of each command's concrete
-  syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
-  where $text$ is delimited by \verb,",\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}\verb,", or
-  \verb,{,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,}, as before.  Multiple
-  marginal comments may be given at the same time.  Here is a simple
-  example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ %
-\isamarkupcmt{a triviality of propositional logic%
-}
-\isanewline
-\ \ %
-\isamarkupcmt{(should not really bother)%
-}
-\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}rule\ impI{\isaliteral{29}{\isacharparenright}}\ %
-\isamarkupcmt{implicit assumption step involved here%
-}
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent The above output has been produced as follows:
-
-\begin{verbatim}
-  lemma "A --> A"
-    -- "a triviality of propositional logic"
-    -- "(should not really bother)"
-    by (rule impI) -- "implicit assumption step involved here"
-\end{verbatim}
-
-  From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
-  command, associated with the macro \verb,\isamarkupcmt, (taking a
-  single argument).
-
-  \medskip Text blocks are introduced by the commands \bfindex{text}
-  and \bfindex{txt}, for theory and proof contexts, respectively.
-  Each takes again a single $text$ argument, which is interpreted as a
-  free-form paragraph in {\LaTeX} (surrounded by some additional
-  vertical space).  This behavior may be changed by redefining the
-  {\LaTeX} environments of \verb,isamarkuptext, or
-  \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
-  text style of the body is determined by \verb,\isastyletext, and
-  \verb,\isastyletxt,; the default setup uses a smaller font within
-  proofs.  This may be changed as follows:
-
-\begin{verbatim}
-  \renewcommand{\isastyletxt}{\isastyletext}
-\end{verbatim}
-
-  \medskip The $text$ part of Isabelle markup commands essentially
-  inserts \emph{quoted material} into a formal text, mainly for
-  instruction of the reader.  An \bfindex{antiquotation} is again a
-  formal object embedded into such an informal portion.  The
-  interpretation of antiquotations is limited to some well-formedness
-  checks, with the result being pretty printed to the resulting
-  document.  Quoted text blocks together with antiquotations provide
-  an attractive means of referring to formal entities, with good
-  confidence in getting the technical details right (especially syntax
-  and types).
-
-  The general syntax of antiquotations is as follows:
-  \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
-  \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
-  for a comma-separated list of options consisting of a $name$ or
-  \texttt{$name$=$value$} each.  The syntax of $arguments$ depends on
-  the kind of antiquotation, it generally follows the same conventions
-  for types, terms, or theorems as in the formal part of a theory.
-
-  \medskip This sentence demonstrates quotations and antiquotations:
-  \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ x} is a well-typed term.
-
-  \medskip\noindent The output above was produced as follows:
-  \begin{ttbox}
-text {\ttlbrace}*
-  This sentence demonstrates quotations and antiquotations:
-  {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
-*{\ttrbrace}
-  \end{ttbox}\vspace{-\medskipamount}
-
-  The notational change from the ASCII character~\verb,%, to the
-  symbol~\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} reveals that Isabelle printed this term, after
-  parsing and type-checking.  Document preparation enables symbolic
-  output by default.
-
-  \medskip The next example includes an option to show the type of all
-  variables.  The antiquotation
-  \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
-  output \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ y{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}b{\isaliteral{2E}{\isachardot}}\ x}.  Type inference has figured
-  out the most general typings in the present theory context.  Terms
-  may acquire different typings due to constraints imposed by their
-  environment; within a proof, for example, variables are given the
-  same types as they have in the main goal statement.
-
-  \medskip Several further kinds of antiquotations and options are
-  available \cite{isabelle-isar-ref}.  Here are a few commonly used
-  combinations:
-
-  \medskip
-
-  \begin{tabular}{ll}
-  \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
-  \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\
-  \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
-  \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
-  \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
-  \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
-  \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
-  \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
-  \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
-  \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
-  \end{tabular}
-
-  \medskip
-
-  Note that \attrdx{no_vars} given above is \emph{not} an
-  antiquotation option, but an attribute of the theorem argument given
-  here.  This might be useful with a diagnostic command like
-  \isakeyword{thm}, too.
-
-  \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
-  particularly interesting.  Embedding uninterpreted text within an
-  informal body might appear useless at first sight.  Here the key
-  virtue is that the string $s$ is processed as Isabelle output,
-  interpreting Isabelle symbols appropriately.
-
-  For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}}, according to the standard interpretation of these symbol
-  (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
-  mathematical notation in both the formal and informal parts of the
-  document very easily, independently of the term language of
-  Isabelle.  Manual {\LaTeX} code would leave more control over the
-  typesetting, but is also slightly more tedious.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-As has been pointed out before (\S\ref{sec:syntax-symbols}),
-  Isabelle symbols are the smallest syntactic entities --- a
-  straightforward generalization of ASCII characters.  While Isabelle
-  does not impose any interpretation of the infinite collection of
-  named symbols, {\LaTeX} documents use canonical glyphs for certain
-  standard symbols \cite{isabelle-isar-ref}.
-
-  The {\LaTeX} code produced from Isabelle text follows a simple
-  scheme.  You can tune the final appearance by redefining certain
-  macros, say in \texttt{root.tex} of the document.
-
-  \begin{enumerate}
-
-  \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
-  \texttt{a\dots z} are output directly, digits are passed as an
-  argument to the \verb,\isadigit, macro, other characters are
-  replaced by specifically named macros of the form
-  \verb,\isacharXYZ,.
-
-  \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
-  \verb,{\isasymXYZ},; note the additional braces.
-
-  \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
-  \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
-  control macro is defined accordingly.
-
-  \end{enumerate}
-
-  You may occasionally wish to give new {\LaTeX} interpretations of
-  named symbols.  This merely requires an appropriate definition of
-  \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
-  \texttt{isabelle.sty} for working examples).  Control symbols are
-  slightly more difficult to get right, though.
-
-  \medskip The \verb,\isabellestyle, macro provides a high-level
-  interface to tune the general appearance of individual symbols.  For
-  example, \verb,\isabellestyle{it}, uses the italics text style to
-  mimic the general appearance of the {\LaTeX} math mode; double
-  quotes are not printed at all.  The resulting quality of typesetting
-  is quite good, so this should be the default style for work that
-  gets distributed to a broader audience.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-By default, Isabelle's document system generates a {\LaTeX} file for
-  each theory that gets loaded while running the session.  The
-  generated \texttt{session.tex} will include all of these in order of
-  appearance, which in turn gets included by the standard
-  \texttt{root.tex}.  Certainly one may change the order or suppress
-  unwanted theories by ignoring \texttt{session.tex} and load
-  individual files directly in \texttt{root.tex}.  On the other hand,
-  such an arrangement requires additional maintenance whenever the
-  collection of theories changes.
-
-  Alternatively, one may tune the theory loading process in
-  \texttt{ROOT.ML} itself: traversal of the theory dependency graph
-  may be fine-tuned by adding \verb,use_thy, invocations, although
-  topological sorting still has to be observed.  Moreover, the ML
-  operator \verb,no_document, temporarily disables document generation
-  while executing a theory loader command.  Its usage is like this:
-
-\begin{verbatim}
-  no_document use_thy "T";
-\end{verbatim}
-
-  \medskip Theory output may be suppressed more selectively, either
-  via \bfindex{tagged command regions} or \bfindex{ignored material}.
-
-  Tagged command regions works by annotating commands with named tags,
-  which correspond to certain {\LaTeX} markup that tells how to treat
-  particular parts of a document when doing the actual type-setting.
-  By default, certain Isabelle/Isar commands are implicitly marked up
-  using the predefined tags ``\emph{theory}'' (for theory begin and
-  end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
-  commands involving ML code).  Users may add their own tags using the
-  \verb,%,\emph{tag} notation right after a command name.  In the
-  subsequent example we hide a particularly irrelevant proof:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadeliminvisible
-\ %
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\begin{isamarkuptext}%
-The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
-  Tags observe the structure of proofs; adjacent commands with the
-  same tag are joined into a single region.  The Isabelle document
-  preparation system allows the user to specify how to interpret a
-  tagged region, in order to keep, drop, or fold the corresponding
-  parts of the document.  See the \emph{Isabelle System Manual}
-  \cite{isabelle-sys} for further details, especially on
-  \texttt{isabelle usedir} and \texttt{isabelle document}.
-
-  Ignored material is specified by delimiting the original formal
-  source with special source comments
-  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped
-  before the type-setting phase, without affecting the formal checking
-  of the theory, of course.  For example, we may hide parts of a proof
-  that seem unfit for general public inspection.  The following
-  ``fully automatic'' proof is actually a fake:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ x\ {\isaliteral{2A}{\isacharasterisk}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent The real source of the proof has been as follows:
-
-\begin{verbatim}
-  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
-\end{verbatim}
-%(*
-
-  \medskip Suppressing portions of printed text demands care.  You
-  should not misrepresent the underlying theory development.  It is
-  easy to invalidate the visible text by hiding references to
-  questionable axioms, for example.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:




