src/HOL/Set.ML
changeset 3905 4bbfbb7a2cd3
parent 3896 ee8ebb74ec00
child 3909 e48e2fb8b895
     1.1 --- a/src/HOL/Set.ML	Thu Oct 16 15:23:53 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Oct 16 15:31:12 1997 +0200
     1.3 @@ -601,7 +601,9 @@
     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 -(* FIXME: Addsimps [image_eqI];*)
     1.8 +(* Addsimps [image_eqI];
     1.9 +   breaks Auth: together with shrK_neq in Shared.ML it loops.  :-(
    1.10 +*)
    1.11  
    1.12  bind_thm ("imageI", refl RS image_eqI);
    1.13