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/ex/CoUnit.thy
changeset 76217 8655344f1cf6
parent 76215 a642599ffdea 
--- a/src/ZF/ex/CoUnit.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/CoUnit.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -37,7 +37,7 @@
   apply (rule subsetI)
   apply (erule counit.coinduct)
    apply (rule subset_refl)
-  apply (unfold counit.con_defs)
+    unfolding counit.con_defs
   apply fast
   done
 
@@ -60,7 +60,7 @@
   by (fast elim!: counit2.free_elims)
 
 lemma Con2_bnd_mono: "bnd_mono(univ(0), \<lambda>x. Con2(x, x))"
-  apply (unfold counit2.con_defs)
+    unfolding counit2.con_defs
   apply (rule bnd_monoI)
    apply (assumption | rule subset_refl QPair_subset_univ QPair_mono)+
   done
@@ -79,7 +79,7 @@
   apply (tactic "safe_tac (put_claset subset_cs \<^context>)")
   apply (erule counit2.cases)
   apply (erule counit2.cases)
-  apply (unfold counit2.con_defs)
+    unfolding counit2.con_defs
   apply (tactic \<open>fast_tac (put_claset subset_cs \<^context>
     addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}]
     addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1\<close>)
isabelle