--- 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,&, ~|~ %$
--- a/doc-src/Ref/defining.tex Thu Jun 17 14:24:43 2004 +0200
+++ b/doc-src/Ref/defining.tex Thu Jun 17 14:26:24 2004 +0200
@@ -240,8 +240,9 @@
num & = & nat ~~|~~ \mbox{\tt-}nat \\
xnum & = & \mbox{\tt \#}nat ~~|~~ \mbox{\tt \#-}nat \\
xstr & = & \mbox{\tt ''~\dots~\tt ''} \\[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, \\
nat & = & digit^+ \\