changeset 79917 | d0205dde00bb |
parent 79905 | 1f509d01c9e3 |
child 79919 | 65e0682cca63 |
--- a/NEWS Fri Mar 15 20:23:50 2024 +0100 +++ b/NEWS Sat Mar 16 09:05:17 2024 +0100 @@ -94,6 +94,16 @@ tranclp_less[simp] tranclp_less_eq[simp] +* Theory "HOL.Wellfounded": + - Added definitions wf_on and wfp_on as restricted versions versions of + wf and wfP respectively. + - Added lemmas. + wf_on_UNIV + wf_on_induct + wfp_on_UNIV + wfp_on_induct + wfp_on_wf_on_eq + * Theory "HOL-Library.Multiset": - Added lemmas. trans_on_mult