updated;

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Fri Jan 04 19:19:51 2002 +0100
@@ -14,7 +14,7 @@
 has as many subtrees as there are natural numbers. How can we possibly
 write down such a tree? Using functional notation! For example, the term
 \begin{isabelle}%
-\ \ \ \ \ Br\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
+\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and

--- a/doc-src/TutorialI/Documents/document/Documents.tex	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Fri Jan 04 19:19:51 2002 +0100
@@ -2,6 +2,130 @@
 \begin{isabellebody}%
 \def\isabellecontext{Documents}%
 \isamarkupfalse%
+%
+\isamarkupsection{Concrete syntax \label{sec:concrete-syntax}%
+}
+\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 \emph{mixfix
+  annotations}\index{mixfix annotations|bold}.  Associated with any
+  kind of name and type declaration, mixfixes give rise both to
+  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.  Any syntax specifications given by
+  end-users need to interact properly with the existing setup of
+  Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further
+  details.  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 declaration forms
+  that already cover the most common situations fairly well.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Infixes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Syntax annotations may be included wherever constants are declared
+  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).
+
+  Infix declarations\index{infix annotations|bold} provide a useful
+  special case of mixfixes, where users need not care about the full
+  details of priorities, nesting, spacing, etc.  The subsequent
+  example of the exclusive-or operation on boolean values illustrates
+  typical infix declarations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{constdefs}\isanewline
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Any curried function with at least two arguments may be associated
+  with infix syntax: \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to
+  the same expression internally.  In partial applications with less
+  than two operands there is a special notation with \isa{op} prefix:
+  \isa{xor} without arguments is represented as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}};
+  combined 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 declaration
+  refers to the bit of concrete syntax to represent the operator,
+  while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the whole
+  construct.
+
+  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.
+
+  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.
+
+  \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.
+  
+  Many binary operations observe the associative law, so the exact
+  grouping does not matter.  Nevertheless, formal statements need be
+  given in a particular format, associativity needs to be treated
+  explicitly within the logic.  Exclusive-or is happens to be
+  associative, as shown below.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ xor{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Such rules may be used in simplification to regroup nested
+  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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkupfalse%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkupfalse%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkuptrue%
+\isamarkuptrue%
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 04 19:19:51 2002 +0100
@@ -206,7 +206,7 @@
 \indexbold{definitions!unfolding}%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jan 04 19:19:51 2002 +0100
@@ -103,7 +103,7 @@
 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
 Embedded in this syntax are the types and formulae of HOL, whose syntax is
-extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
+extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
 To distinguish the two levels, everything
 HOL-specific (terms and types) should be enclosed in
 \texttt{"}\dots\texttt{"}. 

--- a/doc-src/TutorialI/Types/document/Pairs.tex	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Fri Jan 04 19:19:51 2002 +0100
@@ -191,7 +191,7 @@
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent

--- a/doc-src/TutorialI/Types/document/Typedefs.tex	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex	Fri Jan 04 19:19:51 2002 +0100
@@ -123,7 +123,7 @@
 The situation is best summarized with the help of the following diagram,
 where squares denote types and the irregular region denotes a set:
 \begin{center}
-\includegraphics[scale=.8]{Types/typedef}
+\includegraphics[scale=.8]{typedef}
 \end{center}
 Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
 surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:

--- a/doc-src/TutorialI/tutorial.ind	Fri Jan 04 19:19:29 2002 +0100
+++ b/doc-src/TutorialI/tutorial.ind	Fri Jan 04 19:19:51 2002 +0100
@@ -21,9 +21,6 @@
   \item \verb$^$\texttt{*}, \bold{201}
   \item \isasymAnd, \bold{12}, \bold{201}
   \item \ttAnd, \bold{201}
-  \item \isasymrightleftharpoons, 55
-  \item \isasymrightharpoonup, 55
-  \item \isasymleftharpoondown, 55
   \item \emph {$\Rightarrow $}, \bold{5}
   \item \ttlbr, \bold{201}
   \item \ttrbr, \bold{201}
@@ -283,6 +280,7 @@
   \item inductive definitions, 119--137
   \item \isacommand {inductive\_cases} (command), 123, 131
   \item infinitely branching trees, 43
+  \item infix annotations, \bold{54}
   \item \isacommand{infixr} (annotation), 10
   \item \isa {inj_on_def} (theorem), \bold{102}
   \item injections, 102
@@ -326,6 +324,7 @@
   \item LCF, 43
   \item \isa {LEAST} (symbol), 23, 77
   \item least number operator, \see{\protect\isa{LEAST}}{77}
+  \item Leibniz, Gottfried Wilhelm, 53
   \item \isacommand {lemma} (command), 13
   \item \isacommand {lemmas} (command), 85, 94
   \item \isa {length} (symbol), 18
@@ -357,6 +356,7 @@
   \item meta-logic, \bold{72}
   \item methods, \bold{16}
   \item \isa {min} (constant), 23, 24
+  \item mixfix annotations, \bold{53}
   \item \isa {mod} (symbol), 23
   \item \isa {mod_div_equality} (theorem), \bold{143}
   \item \isa {mod_mult_distrib} (theorem), \bold{143}
@@ -419,6 +419,7 @@
   \item \isacommand {prefer} (command), 16, 92
   \item primitive recursion, \see{recursion, primitive}{1}
   \item \isacommand {primrec} (command), 10, 18, 38--43
+  \item \isacommand {print\_syntax} (command), 54
   \item product type, \see{pairs and tuples}{1}
   \item Proof General, \bold{7}
   \item proof state, 12
@@ -544,7 +545,6 @@
   \item surjections, 102
   \item \isa {sym} (theorem), \bold{86}
   \item syntax, 6, 11
-  \item syntax translations, 55--56
 
   \indexspace
 
@@ -569,7 +569,6 @@
   \item tracing the simplifier, \bold{33}
   \item \isa {trancl_trans} (theorem), \bold{105}
   \item transition systems, 109
-  \item \isacommand {translations} (command), 55--56
   \item tries, 44--46
   \item \isa {True} (constant), 5
   \item \isa {truncate} (constant), 155