1.1 --- a/NEWS	Wed Aug 27 18:22:34 2003 +0200
     1.2 +++ b/NEWS	Thu Aug 28 01:56:40 2003 +0200
     1.3 @@ -4,6 +4,20 @@
     1.4  New in this Isabelle release
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
    1.10 +  (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and
    1.11 +  euler (\<a>...\<z>), are now considered normal letters, and can
    1.12 +  therefore be used anywhere where an ASCII letter (a...zA...Z) has
    1.13 +  until now.  Similarily, the symbol digits \<0>...\<9> are now
    1.14 +  considered normal digits.  COMPATIBILITY: This obviously changes the
    1.15 +  parsing of some terms, especially where a symbol has been used as a
    1.16 +  binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x
    1.17 +  will be parsed as an identifier.  Fix it by inserting a space around
    1.18 +  former symbols.  Call 'isatool fixgreek' to try to fix parsing
    1.19 +  errors in existing theory and ML files.
    1.20 +
    1.21  *** HOL ***
    1.22  
    1.23  * 'specification' command added, allowing for definition by