tuned;

--- a/doc-src/IsarRef/basics.tex	Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/basics.tex	Sat Oct 30 20:13:16 1999 +0200
@@ -1,61 +1,7 @@
 
-\chapter{Basic Concepts}\label{ch:basics}
-
-\section{Isabelle/Isar theories}
-
-Isabelle/Isar offers two main improvements over classic Isabelle:
-\begin{enumerate}
-\item A new \emph{theory format}, occasionally referred to as ``new-style
-  theories'', supporting interactive development and unlimited undo operation.
-\item A \emph{formal proof document language} designed to support intelligible
-  semi-automated reasoning.  Instead of putting together unreadable tactic
-  scripts, the author is enabled to express the reasoning in way that is close
-  to mathematical practice.
-\end{enumerate}
-
-The Isar proof language is embedded into the new theory format as a proper
-sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
-$\LEMMANAME$ at the theory level, and left again with the final conclusion
-(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
-well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
-the representing sets.
-
-New-style theory files may still be associated with an ML file consisting of
-plain old tactic scripts.  There is no longer any ML binding generated for the
-theory and theorems, though.  ML functions \texttt{theory}, \texttt{thm}, and
-\texttt{thms} retrieve this information \cite{isabelle-ref}.  Nevertheless,
-migration between classic Isabelle and Isabelle/Isar is relatively easy.  Thus
-users may start to benefit from interactive theory development even before
-they have any idea of the Isar proof language.
-
-\begin{warn}
-  Currently Proof~General does \emph{not} support mixed interactive
-  development of classic Isabelle theory files and tactic scripts, together
-  with Isar documents at the same time.  The ``\texttt{isa}'' and
-  ``\texttt{isar}'' versions of Proof~General are handled as two different
-  theorem proving systems, only one of these may be active.
-\end{warn}
-
-Porting of existing tactic scripts is best done by running two separate
-Proof~General sessions, one for replaying the old script and the other for the
-emerging Isabelle/Isar document.
-
-
-\section{The Isar proof language}
-
-Sorry, this important section has not been written yet!  Refer to
-\cite{Wenzel:1999:TPHOL} for the time being.
-
-\subsection{Commands}
-
-\subsubsection{Isar primitives}
-
-\subsubsection{Derived elements}
-
-
-\subsection{Methods}
-
-\subsection{Attributes}
+%FIXME
+%\chapter{Basic Concepts}\label{ch:basics}
+%\section{The Isar proof language}
 
 %%% Local Variables: 
 %%% mode: latex

--- a/doc-src/IsarRef/generic.tex	Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Sat Oct 30 20:13:16 1999 +0200
@@ -353,7 +353,7 @@
 \end{descr}
 
 
-\subsection{Automatic methods}\label{sec:classical-auto}
+\subsection{Automated methods}\label{sec:classical-auto}
 
 \indexisarmeth{blast}
 \indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
@@ -391,7 +391,7 @@
 \S\ref{sec:classical-mod}.
 
 
-\subsection{Combined automatic methods}
+\subsection{Combined automated methods}
 
 \indexisarmeth{auto}\indexisarmeth{force}
 \begin{matharray}{rcl}
@@ -437,7 +437,7 @@
 \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
   respectively.  By default, rules are considered as \emph{safe}, while a
   single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
-  not applied in the search-oriented automatic methods, but only $rule$).
+  not applied in the search-oriented automated methods, but only $rule$).
   
 \item [$iff$] declares equations both as rewrite rules for the simplifier and
   classical reasoning rules.

--- a/doc-src/IsarRef/intro.tex	Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/intro.tex	Sat Oct 30 20:13:16 1999 +0200
@@ -16,19 +16,18 @@
 end
 \end{ttbox}
 Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the
-\texttt{help} command prints the list of available language elements.
+\texttt{help} command prints a list of available language elements.
 
 Plain TTY-based interaction like this used to be quite feasible with
 traditional tactic based theorem proving, but developing Isar documents
 demands some better user-interface support.  \emph{Proof~General}\index{Proof
   General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
 environment for interactive theorem provers that does all the cut-and-paste
-and forward-backward walk through the document in a very neat way.  Note that
-in Isabelle/Isar, the current position within a partial proof document is
-equally important than the actual proof state.  Thus Proof~General provides
-the canonical working environment for Isabelle/Isar, both for getting
-acquainted (e.g.\ by replaying existing Isar documents) and real production
-work.
+and forward-backward walk through the text in a very neat way.  Note that in
+Isabelle/Isar, the current position within a partial proof document is equally
+important than the actual proof state.  Thus Proof~General provides the
+canonical working environment for Isabelle/Isar, both for getting acquainted
+(e.g.\ by replaying existing Isar documents) and real production work.
 
 \medskip
 
@@ -42,7 +41,8 @@
 You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
 actual installation directory of Proof~General.  From now on, the capital
 \texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
-interface.  Its usage is as follows:
+interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
+  classic Isabelle tactic scripts.}  Its usage is as follows:
 \begin{ttbox}
 Usage: interface [OPTIONS] [FILES ...]
 
@@ -61,9 +61,19 @@
 via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, plain GNU
 Emacs may be configured as follows:
 \begin{ttbox}
-PROOFGENERAL_OPTIONS="-p emacs"
+PROOFGENERAL_OPTIONS="-u false -p emacs"
 \end{ttbox}
 
+Occasionally, a user's \texttt{.emacs} file contains material that is
+incompatible with the version of (X)Emacs that Proof~General prefers.  Then
+proper startup may be still achieved by using the \texttt{-u false}
+option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el}
+  occurring in \texttt{\$ISABELLE_HOME/etc} or
+  \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the
+  Proof~General interface script as well.}
+
+\medskip
+
 With the proper Isabelle interface setup, Isar documents may now be edited by
 visiting appropriate theory files, e.g.\ 
 \begin{ttbox}
@@ -71,18 +81,49 @@
 \end{ttbox}
 Users of XEmacs may note the tool bar for navigating forward and backward
 through the text.  Consult the Proof~General documentation \cite{proofgeneral}
-for further basic command sequences, like ``\texttt{c-c return}'' or
+for further basic command sequences, such as ``\texttt{c-c return}'' or
 ``\texttt{c-c u}''.
 
-\medskip
+
+\section{Isabelle/Isar theories}
+
+Isabelle/Isar offers two main improvements over classic Isabelle:
+\begin{enumerate}
+\item A new \emph{theory format}, occasionally referred to as ``new-style
+  theories'', supporting interactive development and unlimited undo operation.
+\item A \emph{formal proof document language} designed to support intelligible
+  semi-automated reasoning.  Instead of putting together unreadable tactic
+  scripts, the author is enabled to express the reasoning in way that is close
+  to mathematical practice.
+\end{enumerate}
+
+The Isar proof language is embedded into the new theory format as a proper
+sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
+$\LEMMANAME$ at the theory level, and left again with the final conclusion
+(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
+well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
+the representing sets.
 
-Occasionally, a user's \texttt{.emacs} file contains material that is
-incompatible with the version of (X)Emacs that Proof~General prefers.  Then
-proper startup may be still achieved by using the \texttt{-u false}
-option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el}
-  occurring in \texttt{\$ISABELLE_HOME/etc} or
-  \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the
-  Proof~General interface script as well.}
+New-style theory files may still be associated with separate ML files
+consisting of plain old tactic scripts.  There is no longer any ML binding
+generated for the theory and theorems, though.  ML functions \texttt{theory},
+\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
+Nevertheless, migration between classic Isabelle and Isabelle/Isar is
+relatively easy.  Thus users may start to benefit from interactive theory
+development even before they have any idea of the Isar proof language at all.
+
+\begin{warn}
+  Currently Proof~General does \emph{not} support mixed interactive
+  development of classic Isabelle theory files or tactic scripts, together
+  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
+  Proof~General are handled as two different theorem proving systems, only one
+  of these may be active at the same time.
+\end{warn}
+
+Porting of existing tactic scripts is best done by running two separate
+Proof~General sessions, one for replaying the old script and the other for the
+emerging Isabelle/Isar document.
+
 
 \section{How to write Isar proofs anyway?}
 
@@ -93,17 +134,14 @@
 other hand, Isabelle/Isar comes much closer to existing mathematical practice
 of formal proof, so users with less experience in old-style tactical proving,
 but a good understanding of mathematical proof, might cope with Isar even
-better.
+better.  See also \cite{Wenzel:1999:TPHOL} for further background information
+on Isar.
 
-This document really is a \emph{reference manual}.  Nevertheless, we will give
-some discussions of the general principles underlying Isar in
-chapter~\ref{ch:basics}, and provide some clues of how these may be put into
-practice.  Some more background information on Isar is given in
-\cite{Wenzel:1999:TPHOL}.  While there is no proper tutorial on Isabelle/Isar
-available yet, there are several examples distributed with Isabelle.  See
-\texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the
-Isabelle library:
-
+\medskip This really is a \emph{reference manual}.  Nevertheless, we will also
+give some clues of how the concepts introduced here may be put into practice.
+Appendix~\ref{ap:refcard} provides a quick reference card of the most common
+Isabelle/Isar language elements.  There are several examples distributed with
+Isabelle, and available via the Isabelle WWW library:
 \begin{center}\small
   \begin{tabular}{l}
     \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
@@ -111,8 +149,9 @@
   \end{tabular}
 \end{center}
 
-Apart from browsable HTML sources, both Isabelle/Isar sessions also provide
-actual documents (in PDF).
+See \texttt{HOL/Isar_examples} for a collection of introductory examples.
+\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application.  Apart from
+browsable HTML sources, both sessions provide actual documents (in PDF).
 
 %%% Local Variables: 
 %%% mode: latex

--- a/doc-src/IsarRef/isar-ref.tex	Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Sat Oct 30 20:13:16 1999 +0200
@@ -54,14 +54,13 @@
   
   The current version of Isabelle offers Isar as an alternative proof language
   interface layer.  The Isabelle/Isar system provides an interpreter for the
-  Isar formal proof document language.  The input may consist either of
-  \emph{proper document constructors}, or \emph{improper auxiliary commands}
-  (for diagnostics, exploration etc.).  Proof texts consisting of proper
-  document constructors only, admit a purely static reading, thus being
-  intelligible later without requiring dynamic replay that is so typical for
-  traditional proof scripts.  Any of the Isabelle/Isar commands may be
-  executed in single-steps, so basically the interpreter has a proof text
-  debugger already built-in.
+  Isar formal proof document language.  The input may consist either of proper
+  document constructors, or improper auxiliary commands (for diagnostics,
+  exploration etc.).  Proof texts consisting of proper document constructors
+  only, admit a purely static reading, thus being intelligible later without
+  requiring dynamic replay that is so typical for traditional proof scripts.
+  Any of the Isabelle/Isar commands may be executed in single-steps, so
+  basically the interpreter has a proof text debugger already built-in.
   
   Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs
   interface for interactive proof assistants of LFCS Edinburgh, we arrive at a

--- a/doc-src/IsarRef/pure.tex	Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/pure.tex	Sat Oct 30 20:13:16 1999 +0200
@@ -14,10 +14,10 @@
 \emph{improper commands}.  Some proof methods and attributes introduced later
 are classified as improper as well.  Improper Isar language elements, which
 are subsequently marked by $^*$, are often helpful when developing proof
-documents, while their use is usually discouraged for the final outcome.
-Typical examples are diagnostic commands that print terms or theorems
-according to the current context; other commands even emulate old-style
-tactical theorem proving, which facilitates porting of legacy proof scripts.
+documents, while their use is discouraged for the final outcome.  Typical
+examples are diagnostic commands that print terms or theorems according to the
+current context; other commands even emulate old-style tactical theorem
+proving, which facilitates porting of legacy proof scripts.
 
 
 \section{Theory commands}
@@ -33,7 +33,7 @@
 \end{matharray}
 
 Isabelle/Isar ``new-style'' theories are either defined via theory files or
-interactively.  Both actual theory specifications and proofs are handled
+interactively.  Both theory-level specifications and proofs are handled
 uniformly --- occasionally definitional mechanisms even require some explicit
 proof as well.  In contrast, ``old-style'' Isabelle theories support batch
 processing only, with the proof scripts collected in separate ML files.
@@ -67,23 +67,24 @@
   produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
   \S\ref{sec:markup-prf} for further markup commands.
   
-\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
-  existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader system ensures
-  that any of the base theories are properly loaded (and fully up-to-date when
-  $\THEORY$ is executed interactively).  The optional $\isarkeyword{files}$
-  specification declares additional dependencies on ML files.  Unless put in
-  parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see
-  also \S\ref{sec:ML}).  The optional ML file \texttt{$A$.ML} that may be
-  associated with any theory should \emph{not} be included in
-  $\isarkeyword{files}$.
+\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
+  based on existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader
+  system ensures that any of the base theories are properly loaded (and fully
+  up-to-date when $\THEORY$ is executed interactively).  The optional
+  $\isarkeyword{files}$ specification declares additional dependencies on ML
+  files.  Unless put in parentheses, any file will be loaded immediately via
+  $\isarcmd{use}$ (see also \S\ref{sec:ML}).  The optional ML file
+  \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
+  included in $\isarkeyword{files}$, though.
   
 \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
-  mode, so only a limited set of commands may be performed.  Just as for
-  $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
+  mode, so only a limited set of commands may be performed without destroying
+  the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
+  loaded and up-to-date.
   
 \item [$\END$] concludes the current theory definition or context switch.
-  Note that this command cannot be undone, instead the whole theory definition
-  has to be retracted.
+Note that this command cannot be undone, but the whole theory definition has
+to be retracted.
 \end{descr}
 
 
@@ -101,7 +102,7 @@
 \end{matharray}
 
 Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
-another way to insert text into the document generated from a theory (see
+a structured way to insert text into the document generated from a theory (see
 \cite{isabelle-sys} for more information on Isabelle's document preparation
 tools).
 
@@ -127,16 +128,16 @@
   becomes available.  A typical application would be to emit
   \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
   parts from the final document.\footnote{This requires the \texttt{comment}
-    {\LaTeX} package to be included}
+    package to be included in {\LaTeX}.}
 \end{descr}
 
 Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
-macro with the name derived from \verb,\isamarkup, (e.g.\ 
+macro with the name prefixed by \verb,\isamarkup, (e.g.\ 
 \verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
-argument is passed to that macro unchanged, i.e.\ any {\LaTeX} commands may be
-included here.
+argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands
+may be included here as well.
 
-\medskip Further markup commands are available for proofs (see
+\medskip Additional markup commands are available for proofs (see
 \S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
 declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
 elements just preceding the actual theory definition.
@@ -199,8 +200,7 @@
   $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
   as are available in Isabelle/HOL for example, type synonyms are just purely
   syntactic abbreviations without any logical significance.  Internally, type
-  synonyms are fully expanded, as may be observed when printing terms or
-  theorems.
+  synonyms are fully expanded.
 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
   $t$, intended as an actual logical type.  Note that object-logics such as
   Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
@@ -214,7 +214,7 @@
 \end{descr}
 
 
-\subsection{Constants and simple definitions}
+\subsection{Constants and simple definitions}\label{sec:consts}
 
 \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
 \begin{matharray}{rcl}
@@ -248,7 +248,7 @@
 \end{descr}
 
 
-\subsection{Syntax and translations}
+\subsection{Syntax and translations}\label{sec:syn-trans}
 
 \indexisarcmd{syntax}\indexisarcmd{translations}
 \begin{matharray}{rcl}
@@ -274,7 +274,7 @@
   \texttt{output} flag given, all productions are added both to the input and
   output grammar.
 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
-  rules (i.e.\ \emph{macros}): parse/print rules (\texttt{==}), parse rules
+  rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
   (\texttt{=>}), or print rules (\texttt{<=}).  Translation patterns may be
   prefixed by the syntactic category to be used for parsing; the default is
   \texttt{logic}.
@@ -306,7 +306,7 @@
   Everyday work is typically done the hard way, with proper definitions and
   actual theorems.
 \item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
-  Typical applications would also involve attributes, to augment the default
+  Typical applications would also involve attributes, to augment the
   Simplifier context, for example.
 \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
   tags the results as ``lemma''.
@@ -358,7 +358,7 @@
 \begin{descr}
 \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
   The current theory context (if present) is passed down to the ML session,
-  but must not be modified.  Furthermore, the file name is checked with the
+  but may not be modified.  Furthermore, the file name is checked with the
   $\isarkeyword{files}$ dependency declaration given in the theory header (see
   also \S\ref{sec:begin-thy}).
   
@@ -370,32 +370,33 @@
   afterwards.  Thus $text$ may actually change the theory as a side effect.
   
 \item [$\isarkeyword{setup}~text$] changes the current theory context by
-  applying setup functions from $text$, which has to refer to an ML expression
-  of type $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is
-  the canonical way to initialize object-logic specific tools and packages
-  written in ML.
+  applying setup functions from $text$, which refers to an ML expression of
+  type $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the
+  canonical way to initialize object-logic specific tools and packages written
+  in ML.
 \end{descr}
 
 
-\subsection{Syntax translation functions}
+%FIXME remove!?
+%\subsection{Syntax translation functions}
 
-\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
-\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
-\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
-\begin{matharray}{rcl}
-  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
-  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
-  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
-  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
-  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
-  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
-\end{matharray}
+%\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
+%\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
+%\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
+%\begin{matharray}{rcl}
+%  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
+%  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
+%  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
+%  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
+%  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
+%  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
+%\end{matharray}
 
-Syntax translation functions written in ML admit almost arbitrary
-manipulations of Isabelle's inner syntax.  Any of the above commands have a
-single \railqtoken{text} argument that refers to an ML expression of
-appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
-transformations.
+%Syntax translation functions written in ML admit almost arbitrary
+%manipulations of Isabelle's inner syntax.  Any of the above commands have a
+%single \railqtoken{text} argument that refers to an ML expression of
+%appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
+%transformations.
 
 
 \subsection{Oracles}

--- a/doc-src/IsarRef/refcard.tex	Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/refcard.tex	Sat Oct 30 20:13:16 1999 +0200
@@ -1,5 +1,5 @@
 
-\chapter{Isabelle/Isar Quick Reference}
+\chapter{Isabelle/Isar Quick Reference}\label{ap:refcard}
 
 \section{Proof commands}
 
@@ -87,7 +87,8 @@
   \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
   $-$ & \text{no rules} \\
   $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
-  $elim~a@1~\dots~a@n$ & \text{elimination rules} \\[2ex]
+  $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
+  $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
 
   \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
   $simp$ & Simplifier \\

--- a/doc-src/IsarRef/syntax.tex	Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sat Oct 30 20:13:16 1999 +0200
@@ -18,9 +18,9 @@
 
 \begin{warn}
   Note that classic Isabelle theories used to fake parts of the inner type
-  syntax, with complicated rules when quotes may be omitted.  Despite the
-  minor drawback of requiring quotes more often, the syntax of Isabelle/Isar
-  is simpler and more robust in that respect.
+  syntax, with rather complicated rules when quotes may be omitted.  Despite
+  the minor drawback of requiring quotes more often, the syntax of
+  Isabelle/Isar is simpler and more robust in that respect.
 \end{warn}
 
 \medskip
@@ -28,10 +28,9 @@
 Another notable point is proper input termination.  Proof~General demands any
 command to be terminated by ``\texttt{;}''
 (semicolon)\index{semicolon}\index{*;}.  As far as plain Isabelle/Isar is
-concerned, commands may be directly run together, though.  Thus we usually
-omit semicolons when presenting Isar proof text here, in order to gain
-readability.  Note that the documents which automatically generated from
-new-style theories also omit semicolons.
+concerned, commands may be directly run together, though.  In the presentation
+of Isabelle/Isar documents, semicolons are omitted in order to gain
+readability.
 
 
 \section{Lexical matters}\label{sec:lex-syntax}
@@ -65,15 +64,15 @@
 
 The syntax of \texttt{string} admits any characters, including newlines;
 ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) have to be escaped by
-a backslash, though.  Note that ML-style control character notation is
-\emph{not} supported.  The body of \texttt{verbatim} may consist of any text
-not containing \verb|*}|.
+a backslash.  Note that ML-style control characters are \emph{not} supported.
+The body of \texttt{verbatim} may consist of any text not containing
+``\verb|*}|''.
 
 Comments take the form \texttt{(*~\dots~*)} and may be
-nested\footnote{Proof~General may get confused by nested comments, though.},
-just as in ML. Note that these are \emph{source} comments only, which are
-stripped after lexical analysis of the input.  The Isar document syntax also
-provides of \emph{formal comments} that are actually part of the text (see
+nested\footnote{Proof~General may get confused by nested comments.}, just as
+in ML. Note that these are \emph{source} comments only, which are stripped
+after lexical analysis of the input.  The Isar document syntax also provides
+\emph{formal comments} that are actually part of the text (see
 \S\ref{sec:comments}).
 
 
@@ -83,7 +82,7 @@
 terms, and theorem specifications, which have been factored out of the actual
 Isar language elements to be described later.
 
-Note that some of the basic syntactic entities introduced below (such as
+Note that some of the basic syntactic entities introduced below (e.g.\ 
 \railqtoken{name}) act much like tokens rather than plain nonterminals (e.g.\ 
 \railnonterm{sort}), especially for the sake of error messages.  E.g.\ syntax
 elements such as $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
@@ -161,12 +160,12 @@
 The actual inner Isabelle syntax, that of types and terms of the logic, is far
 too sophisticated in order to be modelled explicitly at the outer theory
 level.  Basically, any such entity has to be quoted here to turn it into a
-single token (the parsing and type-checking is performed later).  For
-convenience, a slightly more liberal convention is adopted: quotes may be
+single token (the parsing and type-checking is performed internally later).
+For convenience, a slightly more liberal convention is adopted: quotes may be
 omitted for any type or term that is already \emph{atomic} at the outer level.
 For example, one may write just \texttt{x} instead of \texttt{"x"}.  Note that
-symbolic identifiers such as \texttt{++} are available as well, provided these
-are not superseded by commands or keywords (like \texttt{+}).
+symbolic identifiers (e.g.\ \texttt{++}) are available as well, provided these
+are not superseded by commands or keywords (e.g.\ \texttt{+}).
 
 \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
 \begin{rail}
@@ -193,7 +192,7 @@
 \subsection{Term patterns}\label{sec:term-pats}
 
 Assumptions and goal statements usually admit casual binding of schematic term
-variables by giving (optional) patterns of the form $\ISS{p@1 \dots}{p@n}$.
+variables by giving (optional) patterns of the form $\ISS{p@1\;\dots}{p@n}$.
 There are separate versions available for \railqtoken{term}s and
 \railqtoken{prop}s.  The latter provides a $\CONCLNAME$ part with patterns
 referring the (atomic) conclusion of a rule.
@@ -210,8 +209,10 @@
 \subsection{Mixfix annotations}
 
 Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
-terms.  Some commands such as $\TYPES$ admit infixes only, while $\CONSTS$ and
-$\isarkeyword{syntax}$ support the full range of general mixfixes and binders.
+terms.  Some commands such as $\TYPES$ (see \S\ref{sec:types-pure}) admit
+infixes only, while $\CONSTS$ (see \S\ref{sec:consts}) and
+$\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans}) support the full range of
+general mixfixes and binders.
 
 \indexouternonterm{infix}\indexouternonterm{mixfix}
 \begin{rail}
@@ -232,8 +233,8 @@
 \railnonterm{args} below is parsed by the attribute a second time.  The
 attribute argument specifications may be any sequence of atomic entities
 (identifiers, strings etc.), or properly bracketed argument lists.  Below
-\railqtoken{atom} refers to any atomic entity, including \railtoken{keyword}s
-conforming to \railtoken{symident}.
+\railqtoken{atom} refers to any atomic entity, including any
+\railtoken{keyword} conforming to \railtoken{symident}.
 
 \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
 \begin{rail}
@@ -249,13 +250,13 @@
 
 Theorem specifications come in several flavors: \railnonterm{axmdecl} and
 \railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
-statements, \railnonterm{thmdef} collects lists of existing theorems.
-Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}
-(the former requires an actual singleton result).  Any of these theorem
+statements, while \railnonterm{thmdef} collects lists of existing theorems.
+Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
+the former requires an actual singleton result.  Any of these theorem
 specifications may include lists of attributes both on the left and right hand
 sides; attributes are applied to any immediately preceding theorem.  If names
-are omitted, the theorems are not stored within the theory's theorem database;
-any given attributes are still applied, though.
+are omitted, the theorems are not stored within the theorem database of the
+theory or proof context; any given attributes are still applied, though.
 
 \indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
 \indexouternonterm{thmdef}\indexouternonterm{thmrefs}
@@ -280,12 +281,10 @@
 
 Proof methods are either basic ones, or expressions composed of methods via
 ``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
-``\texttt{?}'' (try once), ``\texttt{+}'' (repeat at least once).  In
-practice, proof methods are usually just a comma separated list of
-\railqtoken{nameref}~\railnonterm{args} specifications.  Thus the syntax is
-similar to that of attributes, with plain parentheses instead of square
-brackets.  Note that parentheses may be dropped for single method
-specifications (with no arguments).
+``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once).  In practice,
+proof methods are usually just a comma separated list of
+\railqtoken{nameref}~\railnonterm{args} specifications.  Note that parentheses
+may be dropped for single method specifications (with no arguments).
 
 \indexouternonterm{method}
 \begin{rail}