# HG changeset patch
# User desharna
# Date 1718607646 -7200
# Node ID 7e0cbc6600b9df1b3e304a2aeb36c77604d7d059
# Parent  94875d8cc8bd2e9b58cf077b7c8cca331f612e0c
removed lemma wellorder.wfP_less

diff -r 94875d8cc8bd -r 7e0cbc6600b9 NEWS
--- 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
diff -r 94875d8cc8bd -r 7e0cbc6600b9 src/HOL/Wellfounded.thy
--- 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)