Added image_eqI to simpset.
authornipkow
Fri, 17 Oct 1997 09:04:02 +0200
changeset 3909 e48e2fb8b895
parent 3908 4f19a40a9343
child 3910 1cc9b8ab161c
Added image_eqI to simpset.
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);