Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Wellfounded.thy
changeset 80019 991557e01814
parent 79999 dca9c237d108
child 80046 38803a6b3357 
--- 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:
isabelle