# HG changeset patch
# User wenzelm
# Date 1473102590 -7200
# Node ID 70554522bf981933de94a6e6e747c83b500e4d22
# Parent  45c8762353dd2e3a484509f6a7999409de6e2c1a
standardized alias;

diff -r 45c8762353dd -r 70554522bf98 src/HOL/ex/Set_Theory.thy
--- 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