NEWS
changeset 62208 ad43b3ab06e4
parent 62205 ca68dc26fbb6
child 62209 009c6e0b44bb
     1.1 --- a/NEWS	Wed Jan 20 13:16:58 2016 +0100
     1.2 +++ b/NEWS	Wed Jan 20 17:14:53 2016 +0100
     1.3 @@ -648,10 +648,15 @@
     1.4  * Library/Multiset:
     1.5    - Renamed multiset inclusion operators:
     1.6        < ~> <#
     1.7 +      > ~> >#
     1.8        \<subset> ~> \<subset>#
     1.9 +      \<supset> ~> \<supset>#
    1.10        <= ~> <=#
    1.11 +      >= ~> >=#
    1.12        \<le> ~> \<le>#
    1.13 +      \<ge> ~> \<ge>#
    1.14        \<subseteq> ~> \<subseteq>#
    1.15 +      \<supseteq> ~> \<supseteq>#
    1.16      INCOMPATIBILITY.
    1.17    - "'a multiset" is no longer an instance of the "order",
    1.18      "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",