# HG changeset patch
# User desharna
# Date 1711533287 -3600
# Node ID b0a46cf73aa478c6559cc8d92276664e78420bf2
# Parent  ac4412562c7b1d27cfc6b2c131c6fedaa76f216f# Parent  991557e0181447a6a0d31fe1b06805502cba10dd
merged

diff -r ac4412562c7b -r b0a46cf73aa4 NEWS
--- a/NEWS	Tue Mar 26 21:44:18 2024 +0100
+++ b/NEWS	Wed Mar 27 10:54:47 2024 +0100
@@ -120,7 +120,7 @@
     predicates 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 ac4412562c7b -r b0a46cf73aa4 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Mar 26 21:44:18 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Mar 27 10:54:47 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: