--- a/NEWS Mon Mar 25 19:27:32 2024 +0100
+++ b/NEWS Mon Mar 25 19:27:53 2024 +0100
@@ -110,7 +110,7 @@
Lemmas wf_def and wfP_def are explicitly provided for backward
compatibility but their usage is discouraged. Minor INCOMPATIBILITY.
- Added wfp as alias for wfP for greater consistency with other predicates
- such as asymp, transp, or totalp.
+ such as asymp, transp, or totalp.
- Added lemmas.
wellorder.wfp_on_less[simp]
wfP_iff_ex_minimal
@@ -120,6 +120,7 @@
wf_on_antimono
wf_on_antimono_strong
wf_on_iff_ex_minimal
+ wf_on_iff_wf
wf_on_induct
wf_on_subset
wfp_on_antimono