# HG changeset patch
# User desharna
# Date 1711442013 -3600
# Node ID 991557e0181447a6a0d31fe1b06805502cba10dd
# Parent  dca9c237d108edc6bce09ff869192025012969b3
renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal

diff -r dca9c237d108 -r 991557e01814 NEWS
--- a/NEWS	Tue Mar 26 09:31:34 2024 +0100
+++ b/NEWS	Tue Mar 26 09:33:33 2024 +0100
@@ -114,7 +114,7 @@
     such as asymp, transp, or totalp.
   - Added lemmas.
       wellorder.wfp_on_less[simp]
-      wfP_iff_ex_minimal
+      wfp_iff_ex_minimal
       wf_iff_ex_minimal
       wf_onE_pf
       wf_onI_pf
diff -r dca9c237d108 -r 991557e01814 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Mar 26 09:31:34 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Mar 26 09:33:33 2024 +0100
@@ -280,7 +280,7 @@
 lemma wfp_on_iff_ex_minimal: "wfp_on A R \<longleftrightarrow> (\<forall>B \<subseteq> A. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B))"
   using wf_on_iff_ex_minimal[of A, to_pred] by simp
 
-lemma wfP_iff_ex_minimal: "wfP R \<longleftrightarrow> (\<forall>B. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B))"
+lemma wfp_iff_ex_minimal: "wfp R \<longleftrightarrow> (\<forall>B. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B))"
   using wfp_on_iff_ex_minimal[of UNIV, simplified] .
 
 lemma wfE_min: