explicit treatment of UTF8 sequences as Isabelle symbols;
authorwenzelm
Fri, 25 Jun 2010 11:48:37 +0200
changeset 37536 c62aa9281101
parent 37535 75de61a479e3
child 37554 6c7399bc0d10
explicit treatment of UTF8 sequences as Isabelle symbols;
NEWS
--- a/NEWS	Thu Jun 24 23:20:47 2010 +0200
+++ b/NEWS	Fri Jun 25 11:48:37 2010 +0200
@@ -4,6 +4,17 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
+a Unicode character is treated as a single symbol, not a sequence of
+non-ASCII bytes as before.  Since Isabelle/ML string literals may
+contain symbols without further backslash escapes, Unicode can now be
+used here as well.  Recall that Symbol.explode in ML provides a
+consistent view on symbols, while raw explode (or String.explode)
+merely give a byte-oriented representation.
+
+
 *** HOL ***
 
 * Some previously unqualified names have been qualified: