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

     2.1 --- a/doc-src/Ref/defining.tex	Thu Jun 17 14:24:43 2004 +0200
     2.2 +++ b/doc-src/Ref/defining.tex	Thu Jun 17 14:26:24 2004 +0200
     2.3 @@ -240,8 +240,9 @@
     2.4  num       & =   & nat ~~|~~ \mbox{\tt-}nat \\
     2.5  xnum      & =   & \mbox{\tt \#}nat ~~|~~ \mbox{\tt \#-}nat \\
     2.6  xstr      & =   & \mbox{\tt ''~\dots~\tt ''} \\[1ex]
     2.7 -letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek \\
     2.8 -quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', ~|~ \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
     2.9 +letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~| \\
    2.10 +      &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
    2.11 +quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
    2.12  latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
    2.13  digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
    2.14  nat & = & digit^+ \\