diff -r 45eee631ea4f -r ad43b3ab06e4 NEWS --- 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: < ~> <# + > ~> ># \ ~> \# + \ ~> \# <= ~> <=# + >= ~> >=# \ ~> \# + \ ~> \# \ ~> \# + \ ~> \# INCOMPATIBILITY. - "'a multiset" is no longer an instance of the "order", "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",