diff -r 3baa6143a9c4 -r e2d44df29c94 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sat Jan 05 01:14:46 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sat Jan 05 01:15:12 2002 +0100
@@ -82,10 +82,10 @@
   \medskip The keyword \isakeyword{infixl} specifies an 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} refers to nesting to the \emph{right}, which
-  would turn \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} into \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.
-  In contrast, a \emph{non-oriented} declaration via
-  \isakeyword{infix} would always demand explicit parentheses.
+  \isakeyword{infixr} refers 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
+  always demand explicit parentheses.
   
   Many binary operations observe the associative law, so the exact
   grouping does not matter.  Nevertheless, formal statements need be
@@ -103,28 +103,234 @@
   expressions as required.  Note that the system would actually print
   the above statement as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}
   (due to nesting to the left).  We have preferred to give the fully
-  parenthesized form in the text for clarity.%
+  parenthesized form in the text for clarity.  Only in rare situations
+  one may consider to force parentheses by use of non-oriented infix
+  syntax; equality would probably be a typical candidate.%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isamarkupsubsection{Mathematical symbols \label{sec:thy-present-symbols}%
+}
 \isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Concrete syntax based on plain ASCII characters has its inherent
+  limitations.  Rich mathematical notation demands a larger repertoire
+  of symbols.  Several standards of extended character sets have been
+  proposed over decades, but none has become universally available so
+  far, not even Unicode\index{Unicode}.
+
+  Isabelle supports a generic notion of
+  \emph{symbols}\index{symbols|bold} as the smallest entities of
+  source text, without referring to internal encodings.  Such
+  ``generalized characters'' may be of one of the following three
+  kinds:
+
+  \begin{enumerate}
+
+  \item Traditional 7-bit ASCII characters.
+
+  \item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
+  \verb,\\,\verb,<,$ident$\verb,>,).
+
+  \item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
+  \verb,\\,\verb,<^,$ident$\verb,>,).
+
+  \end{enumerate}
+
+  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, the
+  \verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
+  $\forall$ --- both by the user-interface of Proof~General + X-Symbol
+  and the Isabelle document processor (see \S\ref{FIXME}).
+
+  A list of standard Isabelle symbols is given in
+  \cite[appendix~A]{isabelle-sys}.  Users may introduce their own
+  interpretation of further symbols by configuring the appropriate
+  front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
+  macros for document preparation.  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.
+
+  \medskip The following version of our \isa{xor} definition uses a
+  standard Isabelle symbol to achieve typographically pleasing output.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{constdefs}\isanewline
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+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 \verb,\,\verb,<oplus>, by hand; the display is adapted
+  immediately after continuing further input.
+
+  \medskip A slightly more refined scheme is to provide alternative
+  syntax via the \emph{print mode}\index{print mode} concept of
+  Isabelle (see also \cite{isabelle-ref}).  By convention, the mode
+  ``$xsymbols$'' is enabled whenever X-Symbol is active.  Consider the
+  following hybrid declaration of \isa{xor}.%
+\end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
 \isamarkupfalse%
+\isacommand{constdefs}\isanewline
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
+\isanewline
 \isamarkupfalse%
+\isacommand{syntax}\ {\isacharparenleft}xsymbols{\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%
 \isamarkupfalse%
-\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Here the \commdx{syntax} command acts like \isakeyword{consts}, but
+  without declaring a logical constant, and with an optional print
+  mode specification.  Note that the type declaration given here
+  merely serves for syntactic purposes, and is not checked for
+  consistency with the real constant.
+
+  \medskip Now we may write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
+  input, while output uses the nicer syntax of $xsymbols$, provided
+  that print mode is presently active.  This scheme is particularly
+  useful for interactive development, with the user typing plain ASCII
+  text, but gaining improved visual feedback from the system (say in
+  current goal output).
+
+  \begin{warn}
+  Using alternative syntax declarations easily results in varying
+  versions of input sources.  Isabelle provides no systematic way to
+  convert alternative 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.%
+\end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
+\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{Prefixes%
+}
 \isamarkuptrue%
-\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Prefix syntax annotations\index{prefix annotation|bold} are just a
+  very degenerate of the general mixfix form \cite{isabelle-ref},
+  without any template arguments or priorities --- just some piece of
+  literal syntax.
+
+  The following example illustrates this idea idea by associating
+  common symbols with the constructors of a currency datatype.%
+\end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{datatype}\ currency\ {\isacharequal}\isanewline
+\ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Here the degenerate 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,\,\verb,<dollar>,.
+
+  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}}}.  Merely the head of the application is
+  subject to our trivial concrete syntax; this form is sufficient to
+  achieve fair conformance to EU~Commission standards of currency
+  notation.
+
+  \medskip Certainly, the same idea of prefix syntax also works for
+  \isakeyword{consts}, \isakeyword{constdefs} etc.  For example, we
+  might introduce a (slightly unrealistic) function to calculate an
+  abstract currency value, by cases on the datatype constructors and
+  fixed exchange rates.%
+\end{isamarkuptext}%
 \isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent The funny symbol encountered here is that of
+  \verb,\<currency>,.%
+\end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isamarkupsubsection{Syntax translations \label{sec:def-translations}%
+}
 \isamarkuptrue%
-\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\index{syntax translations|(}%
+\index{translations@\isacommand {translations} (command)|(}
+Isabelle offers an additional definitional facility,
+\textbf{syntax translations}.
+They resemble macros: upon parsing, the defined concept is immediately
+replaced by its definition.  This effect is reversed upon printing.  For example,
+the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
+\end{isamarkuptext}%
 \isamarkuptrue%
+\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\index{$IsaEqTrans@\isasymrightleftharpoons}
+\noindent
+Internally, \isa{{\isasymnoteq}} never appears.
+
+In addition to \isa{{\isasymrightleftharpoons}} there are
+\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
+for uni-directional translations, which only affect
+parsing or printing.  This tutorial will not cover the details of
+translations.  We have mentioned the concept merely because it
+crops up occasionally; a number of HOL's built-in constructs are defined
+via translations.  Translations are preferable to definitions when the new 
+concept is a trivial variation on an existing one.  For example, we
+don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
+about \isa{{\isacharequal}} still apply.%
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}%
+\end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isamarkupsection{Document preparation%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Batch-mode sessions%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{{\LaTeX} macros%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Structure markup%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Symbols and characters%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
 \end{isabellebody}%