--- a/NEWS Fri Mar 11 17:20:14 2016 +0100
+++ b/NEWS Sat Mar 12 22:04:52 2016 +0100
@@ -53,6 +53,30 @@
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
resemble the f.split naming convention, INCOMPATIBILITY.
+* Characters (type char) are modelled as finite algebraic type
+corresponding to {0..255}.
+
+ - Logical representation:
+ * 0 is instantiated to the ASCII zero character.
+ * All other characters are represented as »Char n«
+ with n being a raw numeral expression less than 256.
+ * Expressions of the form »Char n« with n greater than 255
+ are non-canonical.
+ - Printing and parsing:
+ * Printable characters are printed and parsed as »CHR ''…''«
+ (as before).
+ * The ASCII zero character is printed and parsed as »0«.
+ * All other canonical characters are printed as »CHAR 0xXX«
+ with XX being the hexadecimal character code. »CHAR n«
+ is parsable for every numeral expression n.
+ * Non-canonial characters have no special syntax and are
+ printed as their logical representation.
+ - Explicit conversions from and to the natural numbers are
+ provided as char_of_nat, nat_of_char (as before).
+ - The auxiliary nibble type has been discontinued.
+
+INCOMPATIBILITY.
+
* Multiset membership is now expressed using set_mset rather than count.
- Expressions "count M a > 0" and similar simplify to membership