--- a/NEWS Tue Apr 24 14:17:57 2018 +0000
+++ b/NEWS Tue Apr 24 14:17:58 2018 +0000
@@ -196,6 +196,36 @@
*** HOL ***
+* Clarified relationship of characters, strings and code generation:
+
+ * Type "char" is now a proper datatype of 8-bit values.
+
+ * Conversions "nat_of_char" and "char_of_nat" are gone; use more
+ general conversions "of_char" and "char_of" with suitable
+ type constraints instead.
+
+ * The zero character is just written "CHR 0x00", not
+ "0" any longer.
+
+ * Type "String.literal" (for code generation) is now isomorphic
+ to lists of 7-bit (ASCII) values; concrete values can be written
+ as "STR ''...''" for sequences of printable characters and
+ "ASCII 0x..." for one single ASCII code point given
+ as hexadecimal numeral.
+
+ * Type "String.literal" supports concatenation "... + ..."
+ for all standard target languages.
+
+ * Theory Library/Code_Char is gone; study the explanations concerning
+ "String.literal" in the tutorial on code generation to get an idea
+ how target-language string literals can be converted to HOL string
+ values and vice versa.
+
+ * Imperative-HOL: operation "raise" directly takes a value of type
+ "String.literal" as argument, not type "string".
+
+INCOMPATIBILITY.
+
* Abstract bit operations as part of Main: push_bit, take_bit,
drop_bit.