changed xnum token syntax;
authorwenzelm
Wed, 23 Sep 1998 12:44:30 +0200
changeset 5542 f0c303f53730
parent 5541 f8fb27db4bcd
child 5543 f457121ff50c
changed xnum token syntax;
doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Wed Sep 23 10:56:08 1998 +0200
+++ b/doc-src/Ref/defining.tex	Wed Sep 23 12:44:30 1998 +0200
@@ -236,7 +236,7 @@
 tid       & =   & \mbox{\tt '}id \\
 tvar      & =   & \mbox{\tt ?}tid ~~|~~
                   \mbox{\tt ?}tid\mbox{\tt .}nat \\
-xnum      & =   & \mbox{\tt \#}nat ~~|~~ \mbox{\tt \#\char`\~}nat \\
+xnum      & =   & \mbox{\tt \#}nat ~~|~~ \mbox{\tt \#-}nat \\
 xstr      & =   & \mbox{\tt ''\rm text\tt ''} \\[1ex]
 letter    & =   & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
 digit     & =   & \mbox{one of {\tt 0}\dots {\tt 9}} \\