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/EquivClass.thy
changeset 76217 8655344f1cf6
parent 76216 9fc34f76b4e8 
--- a/src/ZF/EquivClass.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/EquivClass.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -52,7 +52,7 @@
 (*second half*)
 lemma comp_equivI:
     "\<lbrakk>converse(r) O r = r;  domain(r) = A\<rbrakk> \<Longrightarrow> equiv(A,r)"
-apply (unfold equiv_def refl_def sym_def trans_def)
+  unfolding equiv_def refl_def sym_def trans_def
 apply (erule equalityE)
 apply (subgoal_tac "\<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> \<langle>y,x\<rangle> \<in> r", blast+)
 done
isabelle