equal
deleted
inserted
replaced
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 |