Fixed typos.
authorskalberg
Thu, 28 Aug 2003 02:00:16 +0200
changeset 14172 a872d646bf01
parent 14171 0cab06e3bbd0
child 14173 a3690aeb79d4
Fixed typos.
NEWS
--- a/NEWS	Thu Aug 28 01:56:40 2003 +0200
+++ b/NEWS	Thu Aug 28 02:00:16 2003 +0200
@@ -10,7 +10,7 @@
   (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and
   euler (\<a>...\<z>), are now considered normal letters, and can
   therefore be used anywhere where an ASCII letter (a...zA...Z) has
-  until now.  Similarily, the symbol digits \<0>...\<9> are now
+  until now.  Similarily, the symbol digits \<zero>...\<nine> are now
   considered normal digits.  COMPATIBILITY: This obviously changes the
   parsing of some terms, especially where a symbol has been used as a
   binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x