checkpoint;

--- a/doc-src/IsarRef/Makefile	Tue Jul 20 10:34:17 1999 +0200
+++ b/doc-src/IsarRef/Makefile	Tue Jul 20 18:50:46 1999 +0200
@@ -14,7 +14,7 @@
 NAME = isar-ref
 
 FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
-	simplifier.tex classical.tex hol.tex \
+	simplifier.tex classical.tex hol.tex ../isar.sty \
 	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
 
 dvi: $(NAME).dvi

--- a/doc-src/IsarRef/isar-ref.tex	Tue Jul 20 10:34:17 1999 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Tue Jul 20 18:50:46 1999 +0200
@@ -2,11 +2,13 @@
 %% $Id$
 
 \documentclass[12pt]{report}
-\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
+\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../isar,../pdfsetup}
 
 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
+\author{\emph{Markus Wenzel} \\ TU M\"unchen}
 
-\author{\emph{Markus Wenzel} \\ TU M\"unchen}
+\makeindex
+
 
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
@@ -19,7 +21,15 @@
 \railterm{lbrace,rbrace}
 
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
+\railterm{name,nameref,text,type,term,prop,atom}
 
+\makeatletter
+\newcommand{\railtoken}[1]{{\rail@termfont{#1}}}
+\newcommand{\railnonterm}[1]{{\rail@nontfont{#1}}}
+\makeatother
+
+\newcommand\indexoutertoken[1]{\index{#1@\railtoken{#1} (outer syntax)|bold}}
+\newcommand\indexouternonterm[1]{\index{#1@\railnonterm{#1} (outer syntax)|bold}}
 
 \begin{document}
 

--- a/doc-src/IsarRef/syntax.tex	Tue Jul 20 10:34:17 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Tue Jul 20 18:50:46 1999 +0200
@@ -1,28 +1,59 @@
+
+%FIXME
+% - examples (!?)
+
 
 \chapter{Isar document syntax}
 
-\section{Inner versus outer syntax}
+FIXME important note: inner versus outer syntax
 
 \section{Lexical matters}
 
 \section{Common syntax entities}
 
-\subsection{Atoms}
+The Isar proof and theory language syntax has been carefully designed with
+orthogonality in mind.  Many common syntax entities such that those for names,
+terms, types etc.\ have been factored out.  Some of these basic syntactic
+entities usually represent the level of abstraction for error messages: e.g.\ 
+some higher syntax element such as $\CONSTS$ referring to \railtoken{name} or
+\railtoken{type}, would really report a missing \railtoken{name} or
+\railtoken{type} rather than any of its constituent primitive tokens (as
+defined below).  These quasi-tokens are represented in the syntax diagrams
+below using the same font as actual tokens (such as \railtoken{string}).
 
+
+\subsection{Names}
+
+Entity \railtoken{name} usually refers to any name of types, constants,
+theorems, etc.\ to be \emph{declared} or \emph{defined} (so qualified
+identifiers are excluded).  Already existing objects are typically referenced
+by \railtoken{nameref}.
+
+\indexoutertoken{name}\indexoutertoken{nameref}
 \begin{rail}
   name : ident | symident | string
   ;
-
   nameref : name | longident
   ;
-
-  text : nameref | verbatim
-  ;
 \end{rail}
 
+
 \subsection{Comments}
 
+Large chunks of verbatim \railtoken{text} are usually given
+\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\verb|*}|; for convenience,
+any of the smaller text entities (\railtoken{ident}, \railtoken{string} etc.)
+are admitted as well.  Almost any of the Isar commands may be annotated by a
+marginal comment: \texttt{--} \railtoken{text}.  Note that this kind of
+comment is actually part of the language, while source level comments
+\verb|(*|~\verb|*)| are already stripped at the lexical level.  A few commands
+such as $\PROOFNAME$ admit some parts to be mark with a ``level of interest'':
+currently only \texttt{\%} for ``boring, don't read this''.
+
+\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
 \begin{rail}
+  text : verbatim | nameref
+  ;
   comment : (() | '--' text)
   ;
   interest : (() | '\%')
@@ -32,30 +63,141 @@
 
 \subsection{Sorts and arities}
 
+The syntax of sorts and arities is given directly at the outer level.  Note
+that this in contrast to that types and terms (see below).  Only few commands
+ever refer to sorts or arities explicitly.
+
+\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
 \begin{rail}
   sort : nameref | lbrace (nameref * ',') rbrace
   ;
   arity : ( () | '(' (sort + ',') ')' ) sort
   ;
-  simple\-arity : ( () | '(' (sort + ',') ')' ) nameref
+  simplearity : ( () | '(' (sort + ',') ')' ) nameref
+  ;
+\end{rail}
+
+
+\subsection{Types and terms}
+
+The actual inner Isabelle syntax, i.e.\ that of types and terms, is far too
+flexible in order to be modeled explicitly at the outer theory level.
+Basically, any such entity would have to be quoted at the outer level to turn
+it into a single token, with the actual parsing deferred to some functions
+that read and type-check terms etc.\ (note that \railtoken{prop}s will be
+handled differently from plain \railtoken{term}s here).  For convenience, the
+quotes may be omitted for any \emph{atomic} term or type (e.g.\ a single
+variable).
+
+\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
+\begin{rail}
+  type : ident | longident | symident | typefree | typevar | string
+  ;
+  term : ident | longident | symident | var | textvar | nat | string
+  ;
+  prop : term
+  ;
+\end{rail}
+
+Type definitions etc.\ usually refer to \railnonterm{typespec} on the
+left-hand side.  This models basic type constructor application at the outer
+syntax level.  Note that only plain postfix notation is available here, but no
+infixes.
+
+\indexouternonterm{typespec}
+\begin{rail}
+  typespec : (() | typefree | '(' ( typefree + ',' ) ')') name
+  ;
+\end{rail}
+
+
+\subsection{Term patterns}
+
+Statements like $\SHOWNAME$ involve propositions, some others like $\DEFNAME$
+plain terms.  Any of these usually admit automatic binding of schematic text
+variables by giving (optional) patterns $\IS{p@1 \dots p@n}$.  For
+\railtoken{prop}s the $\CONCLNAME$ part refers to the conclusion only, in case
+actual rules are involved, rather than atomic propositions.
+
+\indexouternonterm{termpat}\indexouternonterm{proppat}
+\begin{rail}
+  termpat : '(' (term + 'is' ) ')'
+  ;
+  proppat : '(' (() | (prop + 'is' )) (() | 'concl' (prop + 'is' )) ')'
   ;
 \end{rail}
 
 
-\subsection{Terms and Types}
+\subsection{Mixfix annotations}
+
+Mixfix annotations specify concrete \emph{inner} syntax.  Some commands such
+as $\TYPES$ admit infixes only, while $\CONSTS$ etc.\ support the full range
+of general mixfixes and binders.
 
+\indexouternonterm{infix}\indexouternonterm{mixfix}
 \begin{rail}
-  
+  infix : '(' ('infixl' | 'infixr') (() | string) nat ')'
+  ;
+
+  mixfix : infix | string (() | '[' (nat + ',') ']') (() | nat) |
+  'binder' string (() | '[' (nat + ',') ']') nat
+  ;
 \end{rail}
 
-\subsection{Mixfix annotations}
+
+\subsection{Attributes and theorem specifications}\label{sec:syn-att}
+
+Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
+``semi-inner'' syntax, which does not have to be atomic at the outer level
+unlike that of types and terms.  Instead, the attribute argument
+specifications may be any sequence of atomic entities (identifiers, strings
+etc.), or properly bracketed argument lists.  Below \railtoken{atom} refers to
+any atomic entity (\railtoken{ident}, \railtoken{longident},
+\railtoken{symident} etc.), including keywords that conform to
+\railtoken{symident}, but do not coincide with actual command names.
+
+\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
+\begin{rail}
+  args : (atom | '(' (args *) ')' | '[' (args *) ']' | lbrace (args *) rbrace) *
+  ;
+  attributes : '[' (name args + ',') ']'
+  ;
+\end{rail}
+
+Theorem specifications come in three flavours: \railnonterm{thmdecl} usually
+refers to the result of a goal statement (such as $\SHOWNAME$),
+\railnonterm{thmdef} collects lists of existing theorems (as in $\NOTENAME$),
+\railnonterm{thmref} refers to any list of existing theorems (e.g.\ occurring
+as proof method arguments).  Any of these may include lists of attributes,
+which are applied to the preceding theorem or list of theorems.
+
+\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmref}
+\begin{rail}
+  thmdecl : (() | name) (() | attributes) ':'
+  ;
+  thmdef : (() | name) (() | attributes) '='
+  ;
+  thmref : (name (() | attributes) +)
+  ;
+\end{rail}
 
 
-\subsection{}
+\subsection{Proof methods}\label{sec:syn-meth}
 
-\subsection{}
+Proof methods are either basic ones, or expressions composed of methods via
+``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternatives),
+``\texttt{?}'' (try), ``\texttt{*}'' (repeat, ${} \ge 0$ times),
+``\texttt{+}'' (repeat, ${} > 0$ times).  In practice, proof methods are
+typically just a comma separeted list of \railtoken{name}~\railtoken{args}
+specifications.  Thus the syntax is similar to that of attributes, with plain
+parentheses instead of square brackets (see also \S\ref{sec:syn-att}).  Note
+that parentheses may be dropped for methods without arguments.
 
-\subsection{}
+\indexouternonterm{method}
+\begin{rail}
+  method : (name args | (name | '(' method ')') (() | '?' | '*' | '+')) + (',' | '|')
+  ;
+\end{rail}
 
 
 %%% Local Variables: 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/isar.sty	Tue Jul 20 18:50:46 1999 +0200
@@ -0,0 +1,70 @@
+
+%% $Id$
+
+\usepackage{ifthen}
+
+%Isar language elements
+\newcommand{\I@keyword}[1]{{\mathord{\mathbf{#1}}}}
+\newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
+\newcommand{\I@optoptname}[1]{\ifthenelse{\equal{}{#1}}{}{~[#1\colon]}}
+\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
+\newcommand{\I@optoptmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~[(#1)]}}
+
+\newcommand{\LEMMANAME}{\I@keyword{lemma}}
+\newcommand{\THEOREMNAME}{\I@keyword{theorem}}
+\newcommand{\NOTENAME}{\I@keyword{note}}
+\newcommand{\FROMNAME}{\I@keyword{from}}
+\newcommand{\WITHNAME}{\I@keyword{with}}
+\newcommand{\FIXNAME}{\I@keyword{fix}}
+\newcommand{\ASSUMENAME}{\I@keyword{assume}}
+\newcommand{\PRESUMENAME}{\I@keyword{presume}}
+\newcommand{\HAVENAME}{\I@keyword{have}}
+\newcommand{\SHOWNAME}{\I@keyword{show}}
+\newcommand{\HENCENAME}{\I@keyword{hence}}
+\newcommand{\THUSNAME}{\I@keyword{thus}}
+\newcommand{\PROOFNAME}{\I@keyword{proof}}
+\newcommand{\QEDNAME}{\I@keyword{qed}}
+\newcommand{\BYNAME}{\I@keyword{by}}
+\newcommand{\ISNAME}{\I@keyword{is}}
+\newcommand{\CONCLNAME}{\I@keyword{concl}}
+\newcommand{\LETNAME}{\I@keyword{let}}
+\newcommand{\DEFNAME}{\I@keyword{def}}
+\newcommand{\SUFFNAME}{\I@keyword{suffient}}
+\newcommand{\CMTNAME}{\I@keyword{-{}-}}
+
+\newcommand{\TYPES}{\I@keyword{types}}
+\newcommand{\CONSTS}{\I@keyword{consts}}
+\newcommand{\DEFS}{\I@keyword{defs}}
+\newcommand{\NOTE}[2]{\NOTENAME~#1=#2}
+\newcommand{\FROM}[1]{\FROMNAME~#1}
+\newcommand{\WITH}[1]{\WITHNAME~#1}
+\newcommand{\FIX}[1]{\FIXNAME~#1}
+\newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2}
+\newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2}
+\newcommand{\THEN}{\I@keyword{then}}
+\newcommand{\BEGIN}{\I@keyword{begin}}
+\newcommand{\END}{\I@keyword{end}}
+\newcommand{\BG}{\lceil}
+\newcommand{\EN}{\rfloor}
+\newcommand{\HAVE}[2]{\I@keyword{have}\I@optname{#1}~#2}
+\newcommand{\SHOW}[2]{\I@keyword{show}\I@optname{#1}~#2}
+\newcommand{\HENCE}[2]{\I@keyword{hence}\I@optname{#1}~#2}
+\newcommand{\THUS}[2]{\I@keyword{thus}\I@optname{#1}~#2}
+\newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2}
+\newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
+\newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
+\newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
+\newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
+\newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
+\newcommand{\DOT}{\I@keyword{.}}
+\newcommand{\DDOT}{\I@keyword{.\,.}}
+\newcommand{\DDDOT}{\dots}
+\newcommand{\IS}[1]{(\ISNAME~#1)}
+\newcommand{\LET}[1]{\LETNAME~#1}
+\newcommand{\LETT}[1]{\LETNAME~#1\dt\;}
+\newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
+\newcommand{\SUFF}[1]{\SUFFNAME~#1}
+\newcommand{\ATT}[1]{\ap [#1]}
+\newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
+\newcommand{\ALSO}{\I@keyword{also}}
+\newcommand{\FINALLY}{\I@keyword{finally}}