src/HOL/Set.ML
changeset 3909 e48e2fb8b895
parent 3905 4bbfbb7a2cd3
child 3912 4ed64ad7fb42
     1.1 --- a/src/HOL/Set.ML	Fri Oct 17 09:03:16 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Oct 17 09:04:02 1997 +0200
     1.3 @@ -601,9 +601,7 @@
     1.4  val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
     1.5  by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
     1.6  qed "image_eqI";
     1.7 -(* Addsimps [image_eqI];
     1.8 -   breaks Auth: together with shrK_neq in Shared.ML it loops.  :-(
     1.9 -*)
    1.10 +Addsimps [image_eqI];
    1.11  
    1.12  bind_thm ("imageI", refl RS image_eqI);
    1.13