equal
deleted
inserted
replaced
214 totalp_on_multp |
214 totalp_on_multp |
215 wfP_subset_mset[simp] |
215 wfP_subset_mset[simp] |
216 |
216 |
217 * Theory "HOL-Library.Multiset_Order": |
217 * Theory "HOL-Library.Multiset_Order": |
218 - Added lemmas. |
218 - Added lemmas. |
|
219 asymp_multpHO |
|
220 asymp_not_liftable_to_multpHO |
219 irreflp_on_multpHO[simp] |
221 irreflp_on_multpHO[simp] |
220 multpHO_plus_plus[simp] |
222 multpHO_plus_plus[simp] |
221 totalp_multpDM |
223 totalp_multpDM |
222 totalp_multpHO |
224 totalp_multpHO |
223 totalp_on_multpDM |
225 totalp_on_multpDM |