src/HOL/Set.ML
changeset 3896 ee8ebb74ec00
parent 3842 b55686a7b22c
child 3905 4bbfbb7a2cd3
     1.1 --- a/src/HOL/Set.ML	Thu Oct 16 14:00:20 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Oct 16 14:12:15 1997 +0200
     1.3 @@ -601,6 +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 +(* FIXME: Addsimps [image_eqI];*)
     1.8  
     1.9  bind_thm ("imageI", refl RS image_eqI);
    1.10