
diff -r 892af6538f3d -r cc59ceb0bcb4 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 17:23:35 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 17:23:40 2002 +0100
@@ -58,22 +58,23 @@
   as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this
   turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
 
-  \medskip The keyword \isakeyword{infixl} specifies an infix operator
-  that is nested to the \emph{left}: in iterated applications the more
-  complex expression appears on the left-hand side: \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 to 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.
+  \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, \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.
 
-  The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above 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 (i.e.\ the syntactic priorities of the arguments and
-  result).  As it happens, Isabelle/HOL already uses up many popular
-  combinations of ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}.  Slightly more awkward combinations like the
-  present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions.
+  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
+  (i.e.\ the syntactic priorities of the arguments and result).  As it
+  happens, Isabelle/HOL already uses up many popular combinations of
+  ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}.  As a rule of thumb, more awkward character combinations are
+  more likely to be still available for user extensions, just as our
+  present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
 
   Operator precedence also needs some special considerations.  The
   admissible range is 0--1000.  Very low or high priorities are
@@ -143,11 +144,12 @@
   just type a named entity \verb,\,\verb,<oplus>, by hand; the display
   will be adapted immediately after continuing input.
 
-  \medskip A slightly more refined scheme is to provide alternative
-  syntax via the \bfindex{print mode} concept of Isabelle (see also
-  \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 A slightly more refined scheme of providing alternative
+  syntax forms uses the \bfindex{print mode} concept of Isabelle (see
+  also \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%
@@ -164,12 +166,9 @@
 \begin{isamarkuptext}%
 The \commdx{syntax} command introduced here acts like
   \isakeyword{consts}, but without declaring a logical constant.  The
-  print mode specification (here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}) limits the
-  effect of the syntax annotation concerning output; that alternative
-  production available for input invariably.  Also note that the type
-  declaration in \isakeyword{syntax} merely serves for syntactic
-  purposes, and is \emph{not} checked for consistency with the real
-  constant.
+  print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.  Also note that its type merely serves
+  for syntactic purposes, and is \emph{not} checked for consistency
+  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
@@ -201,7 +200,7 @@
 \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\ {\isasymRightarrow}\ currency}.  An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
+  that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}.  The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
   printed as \isa{{\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
@@ -232,8 +231,8 @@
   \cite{isabelle-ref}.
 
   \medskip A typical example of syntax translations is to decorate
-  relational expressions (i.e.\ set-membership of tuples) with nice
-  symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
+  relational expressions (set-membership of tuples) with symbolic
+  notation, e.g.\ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isanewline
@@ -296,19 +295,23 @@
   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 enables users to write
-  authentic reports on theory developments with little effort, where
-  most consistency checks are handled by the system.
+  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.
-
-  \bigskip The following datatype definition of \isa{{\isacharprime}a\ bintree}
-  models binary trees with nodes being decorated by elements of type
-  \isa{{\isacharprime}a}.%
+  preparation.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{quotation}
+%
+\begin{isamarkuptext}%
+The following datatype definition of \isa{{\isacharprime}a\ bintree} models
+  binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
-\ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
+\ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent The datatype induction rule generated here is of the form
@@ -317,10 +320,15 @@
 \isaindent{\ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
 \isaindent{\ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
 {\isasymLongrightarrow}\ P\ bintree%
-\end{isabelle}
-
-  \bigskip The above document output has been produced by the
-  following theory specification:
+\end{isabelle}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\end{quotation}
+%
+\begin{isamarkuptext}%
+The above document output has been produced by the following theory
+  specification:
 
   \begin{ttbox}
   text {\ttlbrace}*
@@ -338,11 +346,11 @@
   *{\ttrbrace}
   \end{ttbox}
 
-  Here we have augmented the theory by formal comments (via
-  \isakeyword{text} blocks).  The informal parts may again refer to
-  formal entities by means of ``antiquotations'' (such as
+  \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}.%
+  \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -382,8 +390,7 @@
   \texttt{IsaMakefile} \cite{isabelle-sys}.}
 
   \medskip The detailed arrangement of the session sources is as
-  follows.  This may be ignored in the beginning, but some of these
-  files need to be edited in realistic applications.
+  follows.
 
   \begin{itemize}
 
@@ -403,13 +410,13 @@
   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 \texttt{root.tex} does the job in most
-  situations.
+  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 controlled by the same \texttt{IsaMakefile}.
+  several sessions may be managed by the same \texttt{IsaMakefile}.
   See also \cite{isabelle-sys} for further details, especially on
   \texttt{isatool usedir} and \texttt{isatool make}.
 
@@ -430,16 +437,16 @@
   distributed with Isabelle. Further packages may be required in
   particular applications, e.g.\ for unusual mathematical symbols.
 
-  \medskip Additional files for the {\LaTeX} stage may be put into the
-  \texttt{MySession/document} directory, too.  In particular, adding
-  \texttt{root.bib} here (with that specific name) causes an automatic
-  run of \texttt{bibtex} to process a bibliographic database; see also
-  \texttt{isatool document} covered in \cite{isabelle-sys}.
+  \medskip Any additional files for the {\LaTeX} stage go into the
+  \texttt{MySession/document} directory as well.  In particular,
+  adding \texttt{root.bib} (with that specific name) causes an
+  automatic run of \texttt{bibtex} to process a bibliographic
+  database; see also \texttt{isatool document} in \cite{isabelle-sys}.
 
   \medskip Any failure of the document preparation phase in an
   Isabelle batch session leaves the generated sources in their target
   location (as pointed out by the accompanied error message).  This
-  enables users to trace {\LaTeX} problems with the target files at
+  enables users to trace {\LaTeX} problems with the generated files at
   hand.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -474,8 +481,8 @@
   \medskip
 
   From the Isabelle perspective, each markup command takes a single
-  $text$ argument (delimited by \verb,",\dots\verb,", or
-  \verb,{,\verb,*,~\dots~\verb,*,\verb,},).  After stripping any
+  $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
@@ -545,18 +552,18 @@
 %
 \begin{isamarkuptext}%
 Isabelle \bfindex{source comments}, which are of the form
-  \verb,(,\verb,*,~\dots~\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
+  \verb,(,\verb,*,~\isa{{\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,",\dots\verb,", or
-  \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as before.  Multiple
+  where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or
+  \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before.  Multiple
   marginal comments may be given at the same time.  Here is a simple
   example:%
 \end{isamarkuptext}%
@@ -599,7 +606,11 @@
   \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.
+  proofs.  This may be changed as follows:
+
+\begin{verbatim}
+  \renewcommand{\isastyletxt}{\isastyletext}
+\end{verbatim}
 
   \medskip The $text$ part of each of the various markup commands
   considered so far essentially inserts \emph{quoted material} into a
@@ -607,10 +618,10 @@
   \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.  So quoted text blocks together
-  with antiquotations provide very useful means to reference formal
-  entities with good confidence in getting the technical details right
-  (especially syntax and types).
+  printed to the resulting document.  Quoted text blocks together with
+  antiquotations provide very useful means to reference 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
@@ -658,7 +669,7 @@
   \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, print name $a$ \\
+  \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}
 
@@ -702,25 +713,25 @@
   \begin{enumerate}
 
   \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
-  \texttt{a\dots z} are output verbatim, digits are passed as an
+  \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$\verb,>, become
-  \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces).
+  \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, is turned into
+  \verb,{\isasym,$XYZ$\verb,},; note the additional braces.
 
-  \item Named control symbols: \verb,{\isasym,$XYZ$\verb,}, become
-  \verb,\isactrl,$XYZ$ each; subsequent symbols may act as arguments
-  if the corresponding macro is defined accordingly.
+  \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.
 
   \end{enumerate}
 
   Users may occasionally wish to give new {\LaTeX} interpretations of
   named symbols; this merely requires an appropriate definition of
-  \verb,\,\verb,<,$XYZ$\verb,>, (see \texttt{isabelle.sty} for working
-  examples).  Control symbols are slightly more difficult to get
-  right, though.
+  \verb,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (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
@@ -742,10 +753,10 @@
   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 include
-  individual files in \texttt{root.tex} by hand.  On the other hand,
-  such an arrangement requires additional maintenance chores whenever
-  the collection of theories changes.
+  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
@@ -765,9 +776,9 @@
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
   text.  Only the document preparation system is affected, the formal
-  checking the theory is performed unchanged.
+  checking of the theory is performed unchanged.
 
-  In the following example we suppress the slightly formalistic
+  In the subsequent example we suppress the slightly formalistic
   \isakeyword{theory} + \isakeyword{end} surroundings a theory.
 
   \medskip
@@ -785,9 +796,9 @@
   \medskip
 
   Text may be suppressed in a fine-grained manner.  We may even drop
-  vital parts of a formal proof, pretending that things have been
-  simpler than in reality.  For example, the following ``fully
-  automatic'' proof is actually a fake:%
+  vital parts of a proof, pretending that things have been simpler
+  than in reality.  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
@@ -803,18 +814,18 @@
 %(*
 
   \medskip Ignoring portions of printed text does demand some care by
-  the writer.  First of all, the writer is responsible not to
-  obfuscate the underlying formal development in an unduly manner.  It
-  is fairly easy to invalidate the remaining visible text, e.g.\ by
-  referencing questionable formal items (strange definitions,
-  arbitrary axioms etc.) that have been hidden from sight beforehand.
+  the writer.  First of all, the user is responsible not to obfuscate
+  the underlying theory development in an unduly manner.  It is fairly
+  easy to invalidate the visible text, e.g.\ by referencing
+  questionable formal items (strange definitions, arbitrary axioms
+  etc.) that have been hidden from sight beforehand.
 
-  Authentic reports of formal theories, say as part of a library,
-  should refrain from suppressing parts of the text at all.  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.
+  Authentic reports of Isabelle/Isar theories, say as part of a
+  library, should refrain from suppressing parts of the text at all.
+  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,),




