NEWS
changeset 60514 78a82c37b4b2
parent 60497 010c26e24c72
child 60515 484559628038
child 60523 be2d9f5ddc76
equal deleted inserted replaced
60513:55c7316f76d6 60514:78a82c37b4b2
   115     are now available through the "subset_mset" interpretation
   115     are now available through the "subset_mset" interpretation
   116     (e.g. add_mono ~> subset_mset.add_mono).
   116     (e.g. add_mono ~> subset_mset.add_mono).
   117     INCOMPATIBILITY.
   117     INCOMPATIBILITY.
   118   - Renamed conversions:
   118   - Renamed conversions:
   119       set_of ~> set_mset
   119       set_of ~> set_mset
       
   120       multiset_of_set ~> mset_set
   120     INCOMPATIBILITY
   121     INCOMPATIBILITY
   121   - Renamed lemmas:
   122   - Renamed lemmas:
   122       mset_le_def ~> subseteq_mset_def
   123       mset_le_def ~> subseteq_mset_def
   123       mset_less_def ~> subset_mset_def
   124       mset_less_def ~> subset_mset_def
   124       less_eq_multiset.rep_eq ~> subseteq_mset_def
   125       less_eq_multiset.rep_eq ~> subseteq_mset_def