NEWS
changeset 37553 c62aa9281101
parent 37484 b7821e89fb79
child 37591 d3daea901123
     1.1 --- a/NEWS	Thu Jun 24 23:20:47 2010 +0200
     1.2 +++ b/NEWS	Fri Jun 25 11:48:37 2010 +0200
     1.3 @@ -4,6 +4,17 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
    1.10 +a Unicode character is treated as a single symbol, not a sequence of
    1.11 +non-ASCII bytes as before.  Since Isabelle/ML string literals may
    1.12 +contain symbols without further backslash escapes, Unicode can now be
    1.13 +used here as well.  Recall that Symbol.explode in ML provides a
    1.14 +consistent view on symbols, while raw explode (or String.explode)
    1.15 +merely give a byte-oriented representation.
    1.16 +
    1.17 +
    1.18  *** HOL ***
    1.19  
    1.20  * Some previously unqualified names have been qualified: