1.1 --- a/doc-src/IsarRef/syntax.tex	Sat Sep 04 20:55:52 1999 +0200
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Sat Sep 04 20:57:32 1999 +0200
     1.3 @@ -22,6 +22,14 @@
     1.4    robust in that respect.
     1.5  \end{warn}
     1.6  
     1.7 +\medskip
     1.8 +
     1.9 +Another notable point is proper input termination.  Proof~General demands any
    1.10 +command to be terminated by ``\texttt{;}''
    1.11 +(semicolon)\index{semicolon}\index{*;}.  As far as plain Isabelle/Isar is
    1.12 +concerned, commands may be directly run together.  Thus for better
    1.13 +readability, we usually omit semicolons when discussion Isar proof text here.
    1.14 +
    1.15  
    1.16  \section{Lexical matters}\label{sec:lex-syntax}
    1.17  
    1.18 @@ -37,7 +45,6 @@
    1.19    symident & = & sym^+ \\
    1.20    nat & = & digit^+ \\
    1.21    var & = & \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
    1.22 -  textvar & = & \verb,??,ident \\
    1.23    typefree & = & \verb,',ident \\
    1.24    typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
    1.25    string & = & \verb,", ~\dots~ \verb,", \\
    1.26 @@ -105,15 +112,15 @@
    1.27  Large chunks of plain \railqtoken{text} are usually given
    1.28  \railtoken{verbatim}, i.e.\ enclosed in \verb|{*|\dots\verb|*}|.  For
    1.29  convenience, any of the smaller text units conforming to \railqtoken{nameref}
    1.30 -are admitted as well.  Almost any of the Isar commands may be annotated by
    1.31 -some marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
    1.32 -Note that this kind of comment is actually part of the language, while source
    1.33 -level comments \verb|(*|\dots\verb|*)| are stripped at the lexical level.  A
    1.34 -few commands such as $\PROOFNAME$ admit additional markup with a ``level of
    1.35 -interest'': \texttt{\%} followed by an optional number $n$ (default $n = 1$)
    1.36 -indicates that the respective part of the document becomes $n$ levels more
    1.37 -obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon every
    1.38 -hope, who enter here.
    1.39 +are admitted as well.  Almost any of the Isar commands may be annotated by a
    1.40 +marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
    1.41 +Note that the latter kind of comment is actually part of the language, while
    1.42 +source level comments \verb|(*|\dots\verb|*)| are stripped at the lexical
    1.43 +level.  A few commands such as $\PROOFNAME$ admit additional markup with a
    1.44 +``level of interest'': \texttt{\%} followed by an optional number $n$ (default
    1.45 +$n = 1$) indicates that the respective part of the document becomes $n$ levels
    1.46 +more obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon
    1.47 +every hope, who enter here.
    1.48  
    1.49  \indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
    1.50  \begin{rail}
    1.51 @@ -153,13 +160,15 @@
    1.52  token (the parsing and type-checking is performed later).  For convenience, a
    1.53  slightly more liberal convention is adopted: quotes may be omitted for any
    1.54  type or term that is already \emph{atomic} at the outer level.  E.g.\ one may
    1.55 -write just \texttt{x} instead of \texttt{"x"}.
    1.56 +write just \texttt{x} instead of \texttt{"x"}.  Note that symbolic identifiers
    1.57 +such as \texttt{++} are available as well, provided these are not superceded
    1.58 +by commands or keywords (like \texttt{+}).
    1.59  
    1.60  \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
    1.61  \begin{rail}
    1.62    type: nameref | typefree | typevar
    1.63    ;
    1.64 -  term: nameref | var | textvar | nat
    1.65 +  term: nameref | var | nat
    1.66    ;
    1.67    prop: term
    1.68    ;
    1.69 @@ -224,7 +233,7 @@
    1.70  
    1.71  \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
    1.72  \begin{rail}
    1.73 -  atom: nameref | typefree | typevar | var | textvar | nat | keyword
    1.74 +  atom: nameref | typefree | typevar | var | nat | keyword
    1.75    ;
    1.76    arg: atom | '(' args ')' | '[' args ']' | lbrace args rbrace
    1.77    ;
    1.78 @@ -240,7 +249,9 @@
    1.79  Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}
    1.80  (the former requires an actual singleton result).  Any of these theorem
    1.81  specifications may include lists of attributes both on the left and right hand
    1.82 -sides; attributes are applied to any immediately preceding theorem.
    1.83 +sides; attributes are applied to any immediately preceding theorem.  If names
    1.84 +are omitted, the theorems are not stored within the theory's theorem database;
    1.85 +any given attributes are still applied, though.
    1.86  
    1.87  \indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
    1.88  \indexouternonterm{thmdef}\indexouternonterm{thmrefs}
    1.89 @@ -265,8 +276,8 @@
    1.90  
    1.91  Proof methods are either basic ones, or expressions composed of methods via
    1.92  ``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
    1.93 -``\texttt{?}'' (try), ``\texttt{+}'' (at least once).  In practice, proof
    1.94 -methods are usually just a comma separated list of
    1.95 +``\texttt{?}'' (try once), ``\texttt{+}'' (repeat at least once).  In
    1.96 +practice, proof methods are usually just a comma separated list of
    1.97  \railqtoken{nameref}~\railnonterm{args} specifications.  Thus the syntax is
    1.98  similar to that of attributes, with plain parentheses instead of square
    1.99  brackets.  Note that parentheses may be dropped for single method