Modified comment.
authornipkow
Thu Oct 16 15:31:12 1997 +0200 (1997-10-16)
changeset 39054bbfbb7a2cd3
parent 3904 c0d56e4c823e
child 3906 5ae0e1324c56
Modified comment.
src/HOL/Set.ML
     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