--- a/doc-src/IsarRef/syntax.tex Thu Jun 17 14:24:43 2004 +0200
+++ b/doc-src/IsarRef/syntax.tex Thu Jun 17 14:26:24 2004 +0200
@@ -81,8 +81,9 @@
string & = & \verb,", ~\dots~ \verb,", \\
verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex]
- letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek \\
- quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', ~|~ \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
+ letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~|~ \\
+ & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
+ quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$