# HG changeset patch
# User wenzelm
# Date 1087475184 -7200
# Node ID 89cce4e95a22d9a4fe8daecfb06705b62a6c4581
# Parent  014d4e00673960dc51f4ab887f7768dd05a97c75
tuned;

diff -r 014d4e006739 -r 89cce4e95a22 doc-src/IsarRef/syntax.tex
--- 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,&, ~|~  %$
diff -r 014d4e006739 -r 89cce4e95a22 doc-src/Ref/defining.tex
--- 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^+ \\