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/InfDatatype.thy
changeset 76214 0c18df79b1c8
parent 76213 e44d86131648 
--- a/src/ZF/InfDatatype.thy	Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/InfDatatype.thy	Tue Sep 27 17:03:23 2022 +0100
@@ -12,7 +12,7 @@
 
 lemma fun_Vcsucc_lemma:
   assumes f: "f \<in> D -> Vfrom(A,csucc(K))" and DK: "|D| \<le> K" and ICK: "InfCard(K)"
-  shows "\<exists>j. f \<in> D -> Vfrom(A,j) & j < csucc(K)"
+  shows "\<exists>j. f \<in> D -> Vfrom(A,j) \<and> j < csucc(K)"
 proof (rule exI, rule conjI)
   show "f \<in> D \<rightarrow> Vfrom(A, \<Union>z\<in>D. \<mu> i. f`z \<in> Vfrom (A,i))"
     proof (rule Pi_type [OF f])
@@ -46,7 +46,7 @@
 
 lemma subset_Vcsucc:
      "\<lbrakk>D \<subseteq> Vfrom(A,csucc(K));  |D| \<le> K;  InfCard(K)\<rbrakk>
-      \<Longrightarrow> \<exists>j. D \<subseteq> Vfrom(A,j) & j < csucc(K)"
+      \<Longrightarrow> \<exists>j. D \<subseteq> Vfrom(A,j) \<and> j < csucc(K)"
 by (simp add: subset_iff_id fun_Vcsucc_lemma)
 
 (*Version for arbitrary index sets*)
isabelle