
diff -r 83cd2140977d -r 46e3ef8dd9ea doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 00:16:43 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 14 14:39:22 2002 +0100
@@ -8,21 +8,21 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate
-  infrastructure for concrete syntax is that of general
-  \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 elaborate infrastructure for concrete
+  syntax is that of general \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, the whole affair of parser and pretty printer
-  configuration is rather subtle, see also \cite{isabelle-ref}.
-  Syntax specifications given by end-users need to interact properly
-  with the existing setup of Isabelle/Pure and Isabelle/HOL.  It is
+  In full generality, parser and pretty printer configuration is a
+  rather subtle affair, see \cite{isabelle-ref} for details.  Syntax
+  specifications given by end-users need to interact properly with the
+  existing setup of Isabelle/Pure and Isabelle/HOL.  It is
   particularly important to get the precedence of new syntactic
   constructs right, avoiding ambiguities with existing elements.
 
   \medskip Subsequently we introduce a few simple syntax declaration
-  forms that already cover most common situations fairly well.%
+  forms that already cover many common situations fairly well.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -35,8 +35,8 @@
   directly or indirectly, including \isacommand{consts},
   \isacommand{constdefs}, or \isacommand{datatype} (for the
   constructor operations).  Type-constructors may be annotated as
-  well, although this is less frequently encountered in practice
-  (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
+  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, where users need not care about the full details
@@ -58,35 +58,29 @@
   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 string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation
-  refers to the bit of concrete syntax to represent the operator,
+  \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.
+
+  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 spends 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 current
-  arrangement of inner syntax may be inspected via
-  \commdx{print\protect\_syntax}, albeit its output is enormous.
+  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.
 
   Operator precedence also needs some special considerations.  The
   admissible range is 0--1000.  Very low or high priorities are
   basically reserved for the meta-logic.  Syntax of Isabelle/HOL
   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, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50.  User syntax should strive to coexist with common
-  HOL forms, or use the mostly unused range 100--900.
-
-  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.%
+  HOL forms, or use the mostly unused range 100--900.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -119,7 +113,7 @@
   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 really as \isa{{\isasymforall}}.
+  the \verb,\,\verb,<forall>, symbol as \isa{{\isasymforall}}.
 
   A list of standard Isabelle symbols is given in
   \cite[appendix~A]{isabelle-sys}.  Users may introduce their own
@@ -169,41 +163,28 @@
 %
 \begin{isamarkuptext}%
 The \commdx{syntax} command introduced here acts like
-  \isakeyword{consts}, but without declaring a logical constant; an
-  optional print mode specification may be given, too.  Note that the
-  type declaration given above merely serves for syntactic purposes,
-  and is not checked for consistency with the real constant.
+  \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.
 
   \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
   that print mode is active.  Such an arrangement is particularly
   useful for interactive development, where users may type plain ASCII
-  text, but gain improved visual feedback from the system.
-
-  \begin{warn}
-  Alternative syntax declarations are apt to result in varying
-  occurrences of concrete syntax in the input sources.  Isabelle
-  provides no systematic way to convert alternative syntax expressions
-  back and forth; print modes only affect situations where formal
-  entities are pretty printed by the Isabelle process (e.g.\ output of
-  terms and types), but not the original theory text.
-  \end{warn}
-
-  \medskip The following variant makes the alternative \isa{{\isasymoplus}}
-  notation only available for output.  Thus we may enforce input
-  sources to refer to plain ASCII only, but effectively disable
-  cut-and-paste from output at the same time.%
+  text, but gain improved visual feedback from the system.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
 %
 \isamarkupsubsection{Prefix Annotations%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Prefix syntax annotations\index{prefix annotation} are just another
+Prefix syntax annotations\index{prefix annotation} are another
   degenerate 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
@@ -222,8 +203,9 @@
   \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
   printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
-  subject to our concrete syntax.  This simple form already achieves
-  conformance with notational standards of the European Commission.
+  subject to our concrete syntax.  This rather simple form already
+  achieves conformance with notational standards of the European
+  Commission.
 
   Prefix syntax also works for plain \isakeyword{consts} or
   \isakeyword{constdefs}, of course.%
@@ -237,21 +219,21 @@
 \begin{isamarkuptext}%
 Mixfix syntax annotations work well in those situations where
   particular constant application forms need to be decorated by
-  concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before.  Occasionally the relationship between some
-  piece of notation and its internal form is slightly more involved.
-  Here the concept of \bfindex{syntax translations} enters the scene.
+  concrete syntax; e.g.\ \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B}
+  covered before.  Occasionally the relationship between some piece of
+  notation and its internal form is slightly more involved.  Here the
+  concept of \bfindex{syntax translations} enters the scene.
 
   Using the raw \isakeyword{syntax}\index{syntax (command)} command we
   may introduce uninterpreted notational elements, while
-  \commdx{translations} relates input forms with more complex logical
+  \commdx{translations} relate input forms with more complex logical
   expressions.  This essentially provides a simple mechanism for
   syntactic macros; even heavier transformations may be written in ML
   \cite{isabelle-ref}.
 
   \medskip A typical example of syntax translations is to decorate
-  relational expressions (i.e.\ set-membership of tuples) with
-  handsome symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus
-  \isa{x\ {\isasymapprox}\ y}.%
+  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}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isanewline
@@ -310,16 +292,6 @@
   sections, intermediate explanations, definitions, theorems and
   proofs.
 
-  The Isar proof language \cite{Wenzel-PhD}, which is not covered in
-  this book, admits to write formal proof texts that are acceptable
-  both to the machine and human readers at the same time.  Thus
-  marginal comments and explanations may be kept at a minimum.  Even
-  without proper coverage of human-readable proofs, Isabelle document
-  preparation is very useful to produce formally derived texts.
-  Unstructured proof scripts given here may be just ignored by
-  readers, or intentionally suppressed from the text by the writer
-  (see also \S\ref{sec:doc-prep-suppress}).
-
   \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
@@ -337,7 +309,7 @@
 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 theory source files that may contribute to an output document
+  of source files that may contribute to an output document
   eventually.  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
@@ -358,14 +330,14 @@
   The \texttt{isatool 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 that stage usually indicates
+  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
   fall back on DVI output by changing \texttt{usedir} options in
   \texttt{IsaMakefile} \cite{isabelle-sys}.}
 
   \medskip The detailed arrangement of the session sources is as
-  follows:
+  follows; advanced
 
   \begin{itemize}
 
@@ -383,9 +355,9 @@
 
   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.  The generated
-  \texttt{session.tex} will contain {\LaTeX} commands to include all
-  generated files in topologically sorted order, so
+  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.
 
@@ -407,9 +379,9 @@
 
   Especially observe the included {\LaTeX} packages \texttt{isabelle}
   (mandatory), \texttt{isabellesym} (required for mathematical
-  symbols), and the final \texttt{pdfsetup} (provides handsome
-  defaults for \texttt{hyperref}, including URL markup) --- all three
-  are distributed with Isabelle. Further packages may be required in
+  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, e.g.\ for unusual mathematical symbols.
 
   \medskip Additional files for the {\LaTeX} stage may be put into the
@@ -501,10 +473,10 @@
   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
 \end{verbatim}
 
-  \noindent Certainly, this requires to change the default
-  \verb,\documentclass{article}, in \texttt{root.tex} to something
-  that supports the notion of chapters in the first place, e.g.\
-  \verb,\documentclass{report},.
+  \noindent That particular modification requires to change the
+  default \verb,\documentclass{article}, in \texttt{root.tex} to
+  something that supports the notion of chapters in the first place,
+  such as \verb,\documentclass{report},.
 
   \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
   hold the name of the current theory context.  This is particularly
@@ -590,7 +562,7 @@
   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 handsome means to reference formal
+  with antiquotations provide very useful means to reference formal
   entities with good confidence in getting the technical details right
   (especially syntax and types).
 
@@ -640,7 +612,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 validity of fact $a$, print its name \\
+  \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact, print name $a$ \\
   \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
   \end{tabular}
 
@@ -708,10 +680,9 @@
   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 usually be the default
-  style for real production work that gets distributed to a broader
-  audience.%
+  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%
 %
@@ -721,14 +692,14 @@
 %
 \begin{isamarkuptext}%
 By default, Isabelle's document system generates a {\LaTeX} source
-  file for each theory that happens to get 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
-  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.
+  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 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.
 
   Alternatively, one may tune the theory loading process in
   \texttt{ROOT.ML} itself: traversal of the theory dependency graph
@@ -793,11 +764,11 @@
   arbitrary axioms etc.) that have been hidden from sight beforehand.
 
   Authentic reports of formal theories, say as part of a library,
-  usually 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.
+  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,),




