# HG changeset patch
# User nipkow
# Date 877071842 -7200
# Node ID e48e2fb8b8953b623b641b9700b1b5b796cb47b4
# Parent  4f19a40a9343bac9e4f0fa8e2ce94435defaa1bb
Added image_eqI to simpset.

diff -r 4f19a40a9343 -r e48e2fb8b895 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Oct 17 09:03:16 1997 +0200
+++ b/src/HOL/Set.ML	Fri Oct 17 09:04:02 1997 +0200
@@ -601,9 +601,7 @@
 val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
 qed "image_eqI";
-(* Addsimps [image_eqI];
-   breaks Auth: together with shrK_neq in Shared.ML it loops.  :-(
-*)
+Addsimps [image_eqI];
 
 bind_thm ("imageI", refl RS image_eqI);