
diff -r e968745986f1 -r cfcc1f6f21df doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Thu Mar 07 12:03:43 2002 +0100
+++ b/doc-src/IsarRef/syntax.tex	Thu Mar 07 19:04:00 2002 +0100
@@ -1,5 +1,5 @@
 
-\chapter{Syntax primitives}
+\chapter{Syntax Primitives}
 
 The rather generic framework of Isabelle/Isar syntax emerges from three main
 syntactic categories: \emph{commands} of the top-level Isar engine (covering
@@ -40,7 +40,7 @@
 particularly useful in interactive shell sessions to make clear where the
 current command is intended to end.  Otherwise, the interpreter loop will
 continue to issue a secondary prompt ``\verb,#,'' until an end-of-command is
-clearly indicated from the input syntax, e.g.\ encounter of the next command
+clearly recognized from the input syntax, e.g.\ encounter of the next command
 keyword.
 
 Advanced interfaces such as Proof~General \cite{proofgeneral} do not require
@@ -92,12 +92,11 @@
   symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots
 \end{matharray}
 
-The syntax of \railtoken{string} admits any characters, including newlines;
-``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by
-a backslash.  Note that ML-style control characters are \emph{not} supported.
-The body of \railtoken{verbatim} may consist of any text not containing
-``\verb|*}|''; this allows handsome inclusion of quotes without further
-escapes.
+The syntax of $string$ admits any characters, including newlines; ``\verb|"|''
+(double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash.
+Note that ML-style control characters are \emph{not} supported.  The body of
+$verbatim$ may consist of any text not containing ``\verb|*}|''; this allows
+convenient inclusion of quotes without further escapes.
 
 Comments take the form \texttt{(*~\dots~*)} and may in principle be nested,
 just as in ML.  Note that these are \emph{source} comments only, which are
@@ -109,7 +108,8 @@
   Proof~General does not handle nested comments properly; it is also unable to
   keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite
   their rather different meaning.  These are inherent problems of Emacs
-  legacy.
+  legacy.  Users should not be overly aggressive about nesting or alternating
+  these delimiters.
 \end{warn}
 
 \medskip
@@ -209,8 +209,8 @@
 level.  Basically, any such entity has to be quoted to turn it into a 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 just write \texttt{x} instead of \texttt{"x"}.  Note that
+omitted for any type or term that is already atomic at the outer level.  For
+example, one may just write \texttt{x} instead of \texttt{"x"}.  Note that
 symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well,
 provided these have not been superseded by commands or other keywords already
 (e.g.\ \texttt{=} or \texttt{+}).
@@ -338,9 +338,9 @@
 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 theorem database of the
-theory or proof context; any given attributes are still applied, though.
+sides; attributes are applied to any immediately preceding fact.  If names 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}
@@ -365,9 +365,9 @@
 
 Wherever explicit propositions (or term fragments) occur in a proof text,
 casual binding of schematic term variables may be given specified via 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.
+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.
 
 \indexouternonterm{termpat}\indexouternonterm{proppat}
 \begin{rail}
@@ -380,8 +380,8 @@
 Declarations of local variables $x :: \tau$ and logical propositions $a :
 \phi$ represent different views on the same principle of introducing a local
 scope.  In practice, one may usually omit the typing of $vars$ (due to
-type-inference), and the naming of propositions (due to implicit chaining of
-emerging facts).  In any case, Isar proof elements usually admit to introduce
+type-inference), and the naming of propositions (due to implicit references of
+current facts).  In any case, Isar proof elements usually admit to introduce
 multiple such items simultaneously.
 
 \indexouternonterm{vars}\indexouternonterm{props}
@@ -419,8 +419,8 @@
 preparation system (see also \S\ref{sec:document-prep}).
 
 Thus embedding of
-\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a
-text block would cause
+``\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}}''
+within a text block would cause
 \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
 to appear in the final {\LaTeX} document.  Also note that theorem
 antiquotations may involve attributes as well.  For example,
@@ -453,25 +453,32 @@
 \texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
 
 \begin{descr}
+  
 \item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
   specifications may be included as well (see also \S\ref{sec:syn-att}); the
   $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
   useful to suppress printing of schematic variables.
+
 \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
+
 \item [$\at\{term~t\}$] prints a well-typed term $t$.
+
 \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
+  
 \item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
   particularly useful to print portions of text according to the Isabelle
   {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
-  of terms that cannot be parsed or type-checked yet).
+  of terms that should not be parsed or type-checked yet).
+  
 \item [$\at\{goals\}$] prints the current \emph{dynamic} goal state.  This is
-  only for support of tactic-emulation scripts within Isar --- presentation of
-  goal states does not conform to actual human-readable proof documents.
-  
+  mainly for support of tactic-emulation scripts within Isar --- presentation
+  of goal states does not conform to actual human-readable proof documents.
   Please do not include goal states into document output unless you really
   know what you are doing!
+
 \item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
   print the main goal.
+
 \end{descr}
 
 \medskip
@@ -507,9 +514,10 @@
 the above flags are disabled by default, unless changed from ML.
 
 \medskip Note that antiquotations do not only spare the author from tedious
-typing, but also achieve some degree of consistency-checking of informal
-explanations with formal developments, since well-formedness of terms and
-types with respect to the current theory or proof context can be ensured.
+typing of logical entities, but also achieve some degree of
+consistency-checking of informal explanations with formal developments:
+well-formedness of terms and types with respect to the current theory or proof
+context is ensured here.
 
 %%% Local Variables: 
 %%% mode: latex




