--- 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