NEWS
changeset 59986 f38b94549dc8
parent 59967 2fcf41a626f7
child 59991 09be0495dcc2
equal deleted inserted replaced
59985:5574138cf97c 59986:f38b94549dc8
   335   - Renamed multiset ordering:
   335   - Renamed multiset ordering:
   336       <# ~> #<#
   336       <# ~> #<#
   337       <=# ~> #<=#
   337       <=# ~> #<=#
   338       \<subset># ~> #\<subset>#
   338       \<subset># ~> #\<subset>#
   339       \<subseteq># ~> #\<subseteq>#
   339       \<subseteq># ~> #\<subseteq>#
       
   340     INCOMPATIBILITY.
       
   341   - Introduced abbreviations for ill-named multiset operations:
       
   342       <#, \<subset># abbreviate < (strict subset)
       
   343       <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
   340     INCOMPATIBILITY.
   344     INCOMPATIBILITY.
   341   - Renamed
   345   - Renamed
   342       in_multiset_of ~> in_multiset_in_set
   346       in_multiset_of ~> in_multiset_in_set
   343     INCOMPATIBILITY.
   347     INCOMPATIBILITY.
   344   - Removed mcard, is equal to size.
   348   - Removed mcard, is equal to size.