NEWS
changeset 59958 4538d41e8e54
parent 59951 8c49daca5d9f
child 59965 7199ad93b744
equal deleted inserted replaced
59957:5031030aaebe 59958:4538d41e8e54
   328 
   328 
   329 * Theory "Library/Multiset":
   329 * Theory "Library/Multiset":
   330   - Introduced "replicate_mset" operation.
   330   - Introduced "replicate_mset" operation.
   331   - Introduced alternative characterizations of the multiset ordering in
   331   - Introduced alternative characterizations of the multiset ordering in
   332     "Library/Multiset_Order".
   332     "Library/Multiset_Order".
       
   333   - Renamed multiset ordering:
       
   334       <# ~> #<#
       
   335       <=# ~> #<=#
       
   336       \<subset># ~> #\<subset>#
       
   337       \<subseteq># ~> #\<subseteq>#
       
   338     INCOMPATIBILITY.
   333   - Renamed
   339   - Renamed
   334       in_multiset_of ~> in_multiset_in_set
   340       in_multiset_of ~> in_multiset_in_set
   335     INCOMPATIBILITY.
   341     INCOMPATIBILITY.
   336   - Removed mcard, is equal to size.
   342   - Removed mcard, is equal to size.
   337   - Added attributes:
   343   - Added attributes: