--- 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
--- 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: