1.1 --- a/doc-src/IsarRef/syntax.tex	Wed Mar 08 23:37:25 2000 +0100
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Wed Mar 08 23:40:48 2000 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4  within a theory, while \texttt{x + y} is not.
     1.5  
     1.6  \begin{warn}
     1.7 -  Note that classic Isabelle theories used to fake parts of the inner type
     1.8 -  syntax, with rather complicated rules when quotes may be omitted.  Despite
     1.9 +  Note that classic Isabelle theories used to fake parts of the inner syntax
    1.10 +  of types, with rather complicated rules when quotes may be omitted.  Despite
    1.11    the minor drawback of requiring quotes more often, the syntax of
    1.12    Isabelle/Isar is simpler and more robust in that respect.
    1.13  \end{warn}
    1.14 @@ -69,11 +69,11 @@
    1.15  ``\verb|*}|''.
    1.16  
    1.17  Comments take the form \texttt{(*~\dots~*)} and may be
    1.18 -nested\footnote{Proof~General may get confused by nested comments.}, just as
    1.19 -in ML. Note that these are \emph{source} comments only, which are stripped
    1.20 -after lexical analysis of the input.  The Isar document syntax also provides
    1.21 -\emph{formal comments} that are actually part of the text (see
    1.22 -\S\ref{sec:comments}).
    1.23 +nested\footnote{Proof~General may occasionally get confused by nested
    1.24 +  comments.}, just as in ML. Note that these are \emph{source} comments only,
    1.25 +which are stripped after lexical analysis of the input.  The Isar document
    1.26 +syntax also provides \emph{formal comments} that are actually part of the text
    1.27 +(see \S\ref{sec:comments}).
    1.28  
    1.29  
    1.30  \section{Common syntax entities}