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