equal
deleted
inserted
replaced
14 monotone_on_inf_fun |
14 monotone_on_inf_fun |
15 monotone_on_sup_fun |
15 monotone_on_sup_fun |
16 |
16 |
17 * Theory "HOL.Wellfounded": |
17 * Theory "HOL.Wellfounded": |
18 - Added lemmas. |
18 - Added lemmas. |
|
19 wf_on_lex_prod[intro] |
19 wfp_on_iff_wfp |
20 wfp_on_iff_wfp |
20 |
21 |
21 * Theory "HOL-Library.Multiset": |
22 * Theory "HOL-Library.Multiset": |
22 - Renamed lemmas. Minor INCOMPATIBILITY. |
23 - Renamed lemmas. Minor INCOMPATIBILITY. |
23 filter_image_mset ~> filter_mset_image_mset |
24 filter_image_mset ~> filter_mset_image_mset |