NEWS
changeset 60497 010c26e24c72
parent 60489 bfd9b7302a82
child 60514 78a82c37b4b2
equal deleted inserted replaced
60496:12f58a22eb11 60497:010c26e24c72
   113     "semilattice_inf", and "semilattice_sup" type classes. The theorems
   113     "semilattice_inf", and "semilattice_sup" type classes. The theorems
   114     previously provided by these type classes (directly or indirectly)
   114     previously provided by these type classes (directly or indirectly)
   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:
       
   119       set_of ~> set_mset
       
   120     INCOMPATIBILITY
   118   - Renamed lemmas:
   121   - Renamed lemmas:
   119       mset_le_def ~> subseteq_mset_def
   122       mset_le_def ~> subseteq_mset_def
   120       mset_less_def ~> subset_mset_def
   123       mset_less_def ~> subset_mset_def
   121       less_eq_multiset.rep_eq ~> subseteq_mset_def
   124       less_eq_multiset.rep_eq ~> subseteq_mset_def
   122     INCOMPATIBILITY
   125     INCOMPATIBILITY