--- a/NEWS Sun Jun 16 21:54:09 2024 +0200
+++ b/NEWS Mon Jun 17 09:00:46 2024 +0200
@@ -8,6 +8,8 @@
----------------------------
* Theory "HOL.Wellfounded":
+ - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
+ Minor INCOMPATIBILITIES.
- Renamed lemmas. Minor INCOMPATIBILITY.
accp_wfPD ~> accp_wfpD
accp_wfPI ~> accp_wfpI
--- a/src/HOL/Wellfounded.thy Sun Jun 16 21:54:09 2024 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jun 17 09:00:46 2024 +0200
@@ -182,9 +182,6 @@
lemma (in wellorder) wf: "wf {(x, y). x < y}"
unfolding wf_def by (blast intro: less_induct)
-lemma (in wellorder) wfP_less[simp]: "wfp (<)"
- by (simp add: wf wfp_def)
-
lemma (in wellorder) wfp_on_less[simp]: "wfp_on A (<)"
unfolding wfp_on_def
proof (intro allI impI ballI)