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/Zorn.thy
changeset 76217 8655344f1cf6
parent 76216 9fc34f76b4e8 
--- a/src/ZF/Zorn.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Zorn.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -312,7 +312,7 @@
 apply (rule ccontr)
 apply (frule_tac z=z in chain_extend)
   apply (assumption, blast)
-apply (unfold maxchain_def super_def)
+  unfolding maxchain_def super_def
 apply (blast elim!: equalityCE)
 done
 
@@ -346,7 +346,7 @@
      "next \<in> increasing(S) 
       \<Longrightarrow> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
 apply (rule well_ordI)
-apply (unfold Subset_rel_def linear_def)
+  unfolding Subset_rel_def linear_def
 txt\<open>Prove the well-foundedness goal\<close>
 apply (rule wf_onI)
 apply (frule well_ord_TFin_lemma, assumption)
isabelle