equal
deleted
inserted
replaced
106 - Added definitions wf_on and wfp_on as restricted versions versions of |
106 - Added definitions wf_on and wfp_on as restricted versions versions of |
107 wf and wfP respectively. |
107 wf and wfP respectively. |
108 - Added wfp as alias for wfP for greater consistency with other predicates |
108 - Added wfp as alias for wfP for greater consistency with other predicates |
109 such as asymp, transp, or totalp. |
109 such as asymp, transp, or totalp. |
110 - Added lemmas. |
110 - Added lemmas. |
|
111 wellorder.wfp_on_less[simp] |
111 wfP_iff_ex_minimal |
112 wfP_iff_ex_minimal |
112 wf_iff_ex_minimal |
113 wf_iff_ex_minimal |
113 wf_onE_pf |
114 wf_onE_pf |
114 wf_onI_pf |
115 wf_onI_pf |
115 wf_on_UNIV |
116 wf_on_UNIV |