--- a/NEWS Thu Aug 28 02:00:16 2003 +0200
+++ b/NEWS Fri Aug 29 13:18:45 2003 +0200
@@ -7,16 +7,15 @@
*** General ***
* Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
- (\<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 \<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
- will be parsed as an identifier. Fix it by inserting a space around
- former symbols. Call 'isatool fixgreek' to try to fix parsing
- errors in existing theory and ML files.
+ (\<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. 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 will be parsed
+ as an identifier. Fix it by inserting a space around former
+ symbols. Call 'isatool fixgreek' to try to fix parsing errors in
+ existing theory and ML files.
*** HOL ***