equal
deleted
inserted
replaced
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: |
118 - Renamed conversions: |
|
119 multiset_of ~> mset |
|
120 multiset_of_set ~> mset_set |
119 set_of ~> set_mset |
121 set_of ~> set_mset |
120 multiset_of_set ~> mset_set |
|
121 INCOMPATIBILITY |
122 INCOMPATIBILITY |
122 - Renamed lemmas: |
123 - Renamed lemmas: |
123 mset_le_def ~> subseteq_mset_def |
124 mset_le_def ~> subseteq_mset_def |
124 mset_less_def ~> subset_mset_def |
125 mset_less_def ~> subset_mset_def |
125 less_eq_multiset.rep_eq ~> subseteq_mset_def |
126 less_eq_multiset.rep_eq ~> subseteq_mset_def |