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/ZF/WF.thy
changeset 76419 f20865ad6319
parent 76217 8655344f1cf6 
--- 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
isabelle