NEWS
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