--- a/NEWS Fri Feb 26 22:15:09 2016 +0100
+++ b/NEWS Fri Feb 26 22:44:11 2016 +0100
@@ -35,6 +35,23 @@
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
resemble the f.split naming convention, INCOMPATIBILITY.
+* Multiset membership is now expressed using set_mset rather than count.
+ASCII infix syntax ":#" has been discontinued.
+
+ - Expressions "count M a > 0" and similar simplify to membership
+ by default.
+
+ - Converting between "count M a = 0" and non-membership happens using
+ equations count_eq_zero_iff and not_in_iff.
+
+ - Rules count_inI and in_countE obtain facts of the form
+ "count M a = n" from membership.
+
+ - Rules count_in_diffI and in_diff_countE obtain facts of the form
+ "count M a = n + count N a" from membership on difference sets.
+
+INCOMPATIBILITY.
+
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
INCOMPATIBILITY.