NEWS
changeset 62208 ad43b3ab06e4
parent 62205 ca68dc26fbb6
child 62209 009c6e0b44bb
--- a/NEWS	Wed Jan 20 13:16:58 2016 +0100
+++ b/NEWS	Wed Jan 20 17:14:53 2016 +0100
@@ -648,10 +648,15 @@
 * Library/Multiset:
   - Renamed multiset inclusion operators:
       < ~> <#
+      > ~> >#
       \<subset> ~> \<subset>#
+      \<supset> ~> \<supset>#
       <= ~> <=#
+      >= ~> >=#
       \<le> ~> \<le>#
+      \<ge> ~> \<ge>#
       \<subseteq> ~> \<subseteq>#
+      \<supseteq> ~> \<supseteq>#
     INCOMPATIBILITY.
   - "'a multiset" is no longer an instance of the "order",
     "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",