equal
deleted
inserted
replaced
101 wfP_iff_ex_minimal |
101 wfP_iff_ex_minimal |
102 wf_iff_ex_minimal |
102 wf_iff_ex_minimal |
103 wf_onE_pf |
103 wf_onE_pf |
104 wf_onI_pf |
104 wf_onI_pf |
105 wf_on_UNIV |
105 wf_on_UNIV |
|
106 wf_on_antimono |
|
107 wf_on_antimono_strong |
106 wf_on_iff_ex_minimal |
108 wf_on_iff_ex_minimal |
107 wf_on_induct |
109 wf_on_induct |
|
110 wf_on_subset |
108 wfp_on_UNIV |
111 wfp_on_UNIV |
|
112 wfp_on_antimono |
|
113 wfp_on_antimono_strong |
109 wfp_on_iff_ex_minimal |
114 wfp_on_iff_ex_minimal |
110 wfp_on_induct |
115 wfp_on_induct |
|
116 wfp_on_subset |
111 wfp_on_wf_on_eq |
117 wfp_on_wf_on_eq |
112 |
118 |
113 * Theory "HOL-Library.Multiset": |
119 * Theory "HOL-Library.Multiset": |
114 - Added lemmas. |
120 - Added lemmas. |
115 trans_on_mult |
121 trans_on_mult |