# HG changeset patch
# User wenzelm
# Date 906547470 -7200
# Node ID f0c303f5373048e5fd9b5ef8a5f23aafc44bd7dd
# Parent  f8fb27db4bcd8c8a48ed1c833ab7aeac5fd48e15
changed xnum token syntax;

diff -r f8fb27db4bcd -r f0c303f53730 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}} \\