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/AC/Hartog.thy
changeset 76216 9fc34f76b4e8
parent 76215 a642599ffdea 
--- a/src/ZF/AC/Hartog.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/Hartog.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -20,7 +20,7 @@
 lemma Ord_lepoll_imp_ex_well_ord:
      "\<lbrakk>Ord(a); a \<lesssim> X\<rbrakk> 
       \<Longrightarrow> \<exists>Y. Y \<subseteq> X \<and> (\<exists>R. well_ord(Y,R) \<and> ordertype(Y,R)=a)"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (erule exE)
 apply (intro exI conjI)
   apply (erule inj_is_fun [THEN fun_is_rel, THEN image_subset])
@@ -60,7 +60,7 @@
 done
 
 lemma not_Hartog_lepoll_self: "\<not> Hartog(A) \<lesssim> A"
-apply (unfold Hartog_def)
+  unfolding Hartog_def
 apply (rule ex_Ord_not_lepoll [THEN exE])
 apply (rule LeastI, auto) 
 done
isabelle