diff -r 768fab6dae74 -r 3907d597cae6 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Aug 23 09:36:05 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Mon Aug 23 11:43:21 1999 +0200
@@ -13,9 +13,8 @@
 \emph{outer} syntax.  Inner syntax is that of Isabelle types and terms of the
 logic, while outer syntax is that of Isabelle/Isar theories (and proofs).  As
 a general rule, inner syntax entities may occur only as \emph{atomic entities}
-within outer syntax.  For example, quoted string \texttt{"x + y"} and
-identifier \texttt{z} are legal term specifications, while \texttt{x + y} is
-not.
+within outer syntax.  Thus, string \texttt{"x + y"} and identifier \texttt{z}
+are legal term specifications, while \texttt{x + y} is not.
 
 \begin{warn}
   Note that old-style Isabelle theories used to fake parts of the inner type
@@ -42,15 +41,16 @@
   typefree & = & \verb,',ident \\
   typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
   string & = & \verb,", ~\dots~ \verb,", \\
-  verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[2ex]
-
+  verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\
+\end{matharray}
+\begin{matharray}{rcl}
   letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
   digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
   quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
   sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
-   \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \verb,<, ~|~
-   \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \mathtt{\at} ~|~ \verb,^, ~|~ \verb,_, ~|~
-   \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
+   \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~
+   \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \mathtt{\at} ~|~ \\
+  & & \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
 \end{matharray}
 
 The syntax of \texttt{string} admits any characters, including newlines;