NEWS
changeset 14173 a3690aeb79d4
parent 14172 a872d646bf01
child 14175 dbd16ebaf907
     1.1 --- a/NEWS	Thu Aug 28 02:00:16 2003 +0200
     1.2 +++ b/NEWS	Fri Aug 29 13:18:45 2003 +0200
     1.3 @@ -7,16 +7,15 @@
     1.4  *** General ***
     1.5  
     1.6  * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
     1.7 -  (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and
     1.8 -  euler (\<a>...\<z>), are now considered normal letters, and can
     1.9 -  therefore be used anywhere where an ASCII letter (a...zA...Z) has
    1.10 -  until now.  Similarily, the symbol digits \<zero>...\<nine> are now
    1.11 -  considered normal digits.  COMPATIBILITY: This obviously changes the
    1.12 -  parsing of some terms, especially where a symbol has been used as a
    1.13 -  binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x
    1.14 -  will be parsed as an identifier.  Fix it by inserting a space around
    1.15 -  former symbols.  Call 'isatool fixgreek' to try to fix parsing
    1.16 -  errors in existing theory and ML files.
    1.17 +  (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler
    1.18 +  (\<a>...\<z>), are now considered normal letters, and can therefore
    1.19 +  be used anywhere where an ASCII letter (a...zA...Z) has until
    1.20 +  now. COMPATIBILITY: This obviously changes the parsing of some
    1.21 +  terms, especially where a symbol has been used as a binder, say
    1.22 +  '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed
    1.23 +  as an identifier.  Fix it by inserting a space around former
    1.24 +  symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
    1.25 +  existing theory and ML files.
    1.26  
    1.27  *** HOL ***
    1.28