# HG changeset patch
# User wenzelm
# Date 1667505490 -3600
# Node ID f20865ad6319835e4b8ad4c780a5539cbdc19a76
# Parent  2b0ff7c52aa4c540f036e3c90ff45232484a68c0
tuned proofs;

diff -r 2b0ff7c52aa4 -r f20865ad6319 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Thu Nov 03 20:53:21 2022 +0100
+++ b/src/ZF/WF.thy	Thu Nov 03 20:58:10 2022 +0100
@@ -361,12 +361,11 @@
          wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r-``{a}) \<inter> A. wfrec[A](r,x,H))"
   unfolding wf_on_def wfrec_on_def
 apply (erule wfrec [THEN trans])
-apply (simp add: vimage_Int_square cons_subset_iff)
+apply (simp add: vimage_Int_square)
 done
 
 text\<open>Minimal-element characterization of well-foundedness\<close>
-lemma wf_eq_minimal:
-     "wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. \<langle>y,z\<rangle>:r \<longrightarrow> y\<notin>Q))"
-by (unfold wf_def, blast)
+lemma wf_eq_minimal: "wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. \<langle>y,z\<rangle>:r \<longrightarrow> y\<notin>Q))"
+  unfolding wf_def by blast
 
 end