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",