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 bex_rtrancl_min_element_if_wf_on |
|
20 bex_rtrancl_min_element_if_wfp_on |
19 wf_on_lex_prod[intro] |
21 wf_on_lex_prod[intro] |
20 wfp_on_iff_wfp |
22 wfp_on_iff_wfp |
21 |
23 |
22 * Theory "HOL-Library.Multiset": |
24 * Theory "HOL-Library.Multiset": |
23 - Renamed lemmas. Minor INCOMPATIBILITY. |
25 - Renamed lemmas. Minor INCOMPATIBILITY. |