NEWS
changeset 59958 4538d41e8e54
parent 59951 8c49daca5d9f
child 59965 7199ad93b744
     1.1 --- a/NEWS	Wed Apr 08 15:04:06 2015 +0200
     1.2 +++ b/NEWS	Wed Apr 08 15:21:20 2015 +0200
     1.3 @@ -330,6 +330,12 @@
     1.4    - Introduced "replicate_mset" operation.
     1.5    - Introduced alternative characterizations of the multiset ordering in
     1.6      "Library/Multiset_Order".
     1.7 +  - Renamed multiset ordering:
     1.8 +      <# ~> #<#
     1.9 +      <=# ~> #<=#
    1.10 +      \<subset># ~> #\<subset>#
    1.11 +      \<subseteq># ~> #\<subseteq>#
    1.12 +    INCOMPATIBILITY.
    1.13    - Renamed
    1.14        in_multiset_of ~> in_multiset_in_set
    1.15      INCOMPATIBILITY.