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.