
diff -r 7d67b065925e -r 072e9d582db0 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Tue Jan 15 17:54:28 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Tue Jan 15 17:54:31 2002 +0100
@@ -8,18 +8,16 @@
 \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.
+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
+  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.
 
   \medskip Subsequently we introduce a few simple syntax declaration
@@ -33,16 +31,15 @@
 %
 \begin{isamarkuptext}%
 Syntax annotations may be included wherever constants are declared,
-  such as \isacommand{consts} and
-  \isacommand{constdefs} --- 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{{\isasymtimes}} comes to mind).
+  such as \isacommand{consts} and \isacommand{constdefs} --- 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{{\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.%
+  case of mixfixes.  The following example of the exclusive-or
+  operation on boolean values illustrates typical infix declarations.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{constdefs}\isanewline
@@ -52,34 +49,35 @@
 \begin{isamarkuptext}%
 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\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\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this
+  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\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this
   turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
 
   \medskip 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\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}.
-  Similarly, \isakeyword{infixr} specifies nesting to the
-  \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.  In contrast, a \emph{non-oriented} declaration via
-  \isakeyword{infix} would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but
-  demand explicit parentheses to indicate the intended grouping.
+  side, and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}.  Similarly, \isakeyword{infixr} means nesting to the
+  \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.  A \emph{non-oriented} declaration via \isakeyword{infix}
+  would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
+  parentheses to indicate the intended grouping.
 
   The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\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{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}.  Longer character combinations are
-  more likely to be still available for user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
+  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{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}.  Longer
+  character combinations are more likely to be still available for
+  user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\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{{\isacharequal}} is
-  centered at 50; logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50; algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) are above 50.  User syntax should strive to coexist with common
-  HOL forms, or use the mostly unused range 100--900.%
+  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{{\isacharequal}} is centered at
+  50; logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are
+  below 50; algebraic ones (like \isa{{\isacharplus}} and \isa{{\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%
 %
@@ -88,14 +86,13 @@
 \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 supports a generic notion of \bfindex{symbols} as the
-  smallest entities of source text, without referring to internal
-  encodings.  There are three kinds of such ``generalized
-  characters'':
+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}
 
@@ -109,13 +106,13 @@
 
   Here $ident$ may be any identifier according to the usual Isabelle
   conventions.  This results in an infinite store of symbols, whose
-  interpretation is left to further front-end tools.  For example,
-  both 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{{\isasymforall}}.
+  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{{\isasymforall}}.
 
   A list of standard Isabelle symbols is given in
-  \cite[appendix~A]{isabelle-sys}.  You may introduce their own
+  \cite[appendix~A]{isabelle-sys}.  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
@@ -124,7 +121,7 @@
   printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
   output as \isa{A\isactrlsup {\isasymstar}}.
 
-  \medskip Replacing our definition of \isa{xor} by the following 
+  \medskip Replacing our definition of \isa{xor} by the following
   specifies a Isabelle symbol for the new operator:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -138,15 +135,14 @@
 \begin{isamarkuptext}%
 \noindent The X-Symbol package within Proof~General provides several
   input methods to enter \isa{{\isasymoplus}} in the text.  If all fails one may
-  just type a named entity \verb,\,\verb,<oplus>, by hand; the 
-  corresponding symbol will immediately be displayed.
+  just type a named entity \verb,\,\verb,<oplus>, by hand; the
+  corresponding symbol will be displayed after further input.
 
-  \medskip 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}:%
+  \medskip 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%
 \isamarkupfalse%
@@ -168,10 +164,10 @@
   with the real constant.
 
   \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
-  input, while output uses the nicer syntax of $xsymbols$, provided
+  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.%
+  useful for interactive development, where users may type ASCII text
+  and see mathematical symbols displayed during proofs.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -180,11 +176,10 @@
 \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 bits of literal
-  syntax.  The following example illustrates this idea idea by
-  associating common symbols with the constructors of a datatype.%
+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}\ currency\ {\isacharequal}\isanewline
@@ -203,7 +198,7 @@
   achieves conformance with notational standards of the European
   Commission.
 
-  Prefix syntax also works for \isakeyword{consts} or
+  Prefix syntax works the same way for \isakeyword{consts} or
   \isakeyword{constdefs}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -213,22 +208,22 @@
 \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\ {\isasymoplus}\ B}.  Occasionally, the relationship between some piece of
-  notation and its internal form is more complicated.  Here we need
-  \bfindex{syntax translations}.
+Mixfix syntax annotations merely decorate particular constant
+  application forms with concrete syntax, for instance replacing \
+  \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}.  Occasionally, the
+  relationship between some piece of notation and its internal form is
+  more complicated.  Here we need \bfindex{syntax translations}.
 
   Using the \isakeyword{syntax}\index{syntax (command)}, command we
   introduce uninterpreted notational elements.  Then
   \commdx{translations} relate input forms to complex logical
-  expressions.  This provides a simple mechanism for
-  syntactic macros; even heavier transformations may be written in ML
+  expressions.  This provides a simple mechanism for syntactic macros;
+  even heavier transformations may be written in ML
   \cite{isabelle-ref}.
 
   \medskip A typical use of syntax translations is to introduce
-  relational notation for membership in a set of pair, 
-  replacing \ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.%
+  relational notation for membership in a set of pair, replacing \
+  \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isanewline
@@ -243,8 +238,8 @@
 %
 \begin{isamarkuptext}%
 \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
-  not matter, as long as it is not used elsewhere.  Prefixing
-  an underscore is a common convention.  The \isakeyword{translations}
+  not matter, as long as it is not used elsewhere.  Prefixing an
+  underscore is a common convention.  The \isakeyword{translations}
   declaration already uses concrete syntax on the left-hand side;
   internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
   \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
@@ -267,11 +262,10 @@
   replaced by the ``definition'' upon parsing; the effect is reversed
   upon printing.
 
-  This sort of translation is appropriate when the 
-  defined concept is a trivial variation on an
-  existing one.  On the other hand, syntax translations do not scale
-  up well to large hierarchies of concepts.  Translations
-  do not replace definitions!%
+  This sort of translation is appropriate when the defined concept is
+  a trivial variation on an existing one.  On the other hand, syntax
+  translations do not scale up well to large hierarchies of concepts.
+  Translations do not replace definitions!%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -281,19 +275,18 @@
 %
 \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.
+  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.
+  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.%
@@ -324,8 +317,7 @@
 \end{quotation}
 %
 \begin{isamarkuptext}%
-The above document output has been produced by the following theory
-  specification:
+\noindent The above document output has been produced as follows:
 
   \begin{ttbox}
   text {\ttlbrace}*
@@ -336,16 +328,17 @@
 
   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}
+  \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
+  (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}%
@@ -359,11 +352,11 @@
 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/browser_info,).
+  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/browser_info,).
 
   \medskip The easiest way to manage Isabelle sessions is via
   \texttt{isatool mkdir} (generates an initial session source setup)
@@ -382,7 +375,7 @@
   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.\footnote{Especially
-  make sure that \texttt{pdflatex} is present; if all fails one may
+  make sure that \texttt{pdflatex} is present; if in doubt one may
   fall back on DVI output by changing \texttt{usedir} options in
   \texttt{IsaMakefile} \cite{isabelle-sys}.}
 
@@ -421,8 +414,8 @@
   \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
+  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
@@ -437,15 +430,14 @@
 
   \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{isatool document} \cite{isabelle-sys}.
+  adding a file named \texttt{root.bib} causes an automatic run of
+  \texttt{bibtex} to process a bibliographic database; see also
+  \texttt{isatool 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.%
+  location, identified by the accompanying error message.  This lets
+  you trace {\LaTeX} problems with the generated files at hand.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -482,9 +474,9 @@
   $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or
   \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},).  After stripping any
   surrounding white space, the argument is passed to a {\LaTeX} macro
-  \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}.  These macros
-  are defined in \verb,isabelle.sty, according to the meaning given in
-  the rightmost column above.
+  \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
@@ -513,22 +505,20 @@
   theorem main: \dots
 
   end
-  \end{ttbox}
+  \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,.
+  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},.
+  \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
@@ -611,27 +601,27 @@
   \renewcommand{\isastyletxt}{\isastyletext}
 \end{verbatim}
 
-  \medskip The $text$ part of these 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).
+  \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$}.  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.
+  \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{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
+  \medskip This sentence demonstrates quotations and antiquotations:
+  \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
 
   \medskip\noindent The output above was produced as follows:
   \begin{ttbox}
@@ -639,22 +629,21 @@
   This sentence demonstrates quotations and antiquotations:
   {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
 *{\ttrbrace}
-  \end{ttbox}
+  \end{ttbox}\vspace{-\medskipamount}
 
   The notational change from the ASCII character~\verb,%, to the
-  symbol~\isa{{\isasymlambda}} reveals that Isabelle printed this term, 
-  after parsing and type-checking.  Document preparation
-  enables symbolic output by default.
+  symbol~\isa{{\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 modify Isabelle's
   \verb,show_types, flag.  The antiquotation
-  \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces 
-  the output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\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.
+  \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
+  output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\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-sys}.  Here are a few commonly used
@@ -690,8 +679,9 @@
   For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\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.  Manual {\LaTeX} code would leave more control
-  over the typesetting, but is also slightly more tedious.%
+  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%
 %
@@ -707,9 +697,9 @@
   named symbols, {\LaTeX} documents use canonical glyphs for certain
   standard symbols \cite[appendix~A]{isabelle-sys}.
 
-  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.
+  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}
 
@@ -719,18 +709,18 @@
   replaced by specifically named macros of the form
   \verb,\isacharXYZ,.
 
-  \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, is turned into
-  \verb,{\isasym,$XYZ$\verb,},; note the additional braces.
+  \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
+  \verb,{\isasymXYZ},; note the additional braces.
 
-  \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, is
-  turned into \verb,\isactrl,$XYZ$; subsequent symbols may act as
-  arguments if the corresponding macro is defined accordingly.
+  \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,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (see
+  \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
   \texttt{isabelle.sty} for working examples).  Control symbols are
   slightly more difficult to get right, though.
 
@@ -764,23 +754,22 @@
   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:
+  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.
-  Research articles and slides usually do not include the
-  formal content in full.  In order to delimit \bfindex{ignored
-  material}, special source comments
-  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
-  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
-  text.  Only document preparation is affected; the formal
-  checking of the theory is unchanged.
+  \medskip Theory output may be suppressed more selectively.  Research
+  articles and slides usually do not include the formal content in
+  full.  Delimiting \bfindex{ignored material} by the special source
+  comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
+  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
+  preparation system to suppress these parts; the formal checking of
+  the theory is unchanged.
 
-  In this example, we suppress  a theory's uninteresting
-  \isakeyword{theory} and \isakeyword{end} brackets:
+  In this example, we hide a theory's \isakeyword{theory} and
+  \isakeyword{end} brackets:
 
   \medskip
 
@@ -798,8 +787,8 @@
 
   Text may be suppressed in a fine-grained manner.  We may even hide
   vital parts of a proof, pretending that things have been simpler
-  than they really were.  For example, this ``fully automatic'' proof is
-  actually a fake:%
+  than they really were.  For example, this ``fully automatic'' proof
+  is actually a fake:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
@@ -814,18 +803,16 @@
 \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.
+  \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.
 
   Authentic reports of Isabelle/Isar theories, say as part of a
-  library, should suppress nothing.
-  Other users may need the full information for their own derivative
-  work.  If a particular formalization appears inadequate for general
-  public coverage, it is often more appropriate to think of a better
-  way in the first place.
+  library, should suppress nothing.  Other users may need the full
+  information for their own derivative work.  If a particular
+  formalization appears inadequate for general public coverage, it is
+  often more appropriate to think of a better way in the first place.
 
   \medskip Some technical subtleties of the
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),




