Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
standardized alias;
authorwenzelm
Mon, 05 Sep 2016 21:09:50 +0200
changeset 63804 70554522bf98
parent 63796 45c8762353dd
child 63805 c272680df665
standardized alias;
src/HOL/ex/Set_Theory.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/Set_Theory.thy	Mon Sep 05 18:40:29 2016 +0200
+++ b/src/HOL/ex/Set_Theory.thy	Mon Sep 05 21:09:50 2016 +0200
@@ -108,7 +108,7 @@
     apply (rule_tac [2] inj_on_inv_into)
     apply (erule subset_inj_on [OF _ subset_UNIV])
    apply blast
-  apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
+  apply (erule ssubst, subst double_complement, erule image_inv_f_f [symmetric])
   done
isabelle