NEWS
changeset 59958 4538d41e8e54
parent 59951 8c49daca5d9f
child 59965 7199ad93b744
--- a/NEWS	Wed Apr 08 15:04:06 2015 +0200
+++ b/NEWS	Wed Apr 08 15:21:20 2015 +0200
@@ -330,6 +330,12 @@
   - Introduced "replicate_mset" operation.
   - Introduced alternative characterizations of the multiset ordering in
     "Library/Multiset_Order".
+  - Renamed multiset ordering:
+      <# ~> #<#
+      <=# ~> #<=#
+      \<subset># ~> #\<subset>#
+      \<subseteq># ~> #\<subseteq>#
+    INCOMPATIBILITY.
   - Renamed
       in_multiset_of ~> in_multiset_in_set
     INCOMPATIBILITY.