diff -r eb5586526bc9 -r a73f5a63f197 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Sat Nov 15 18:41:06 1997 +0100
+++ b/src/HOL/Set.ML	Sun Nov 16 16:18:31 1997 +0100
@@ -610,16 +610,6 @@
 qed "image_iff";
 
 
-goal Set.thy "(! x : f `` A. P x) = (! a:A. P(f a))";
-by (Blast_tac 1);
-qed "ball_image";
-
-goal Set.thy "(? x : f `` A. P x) = (? a:A. P(f a))";
-by (Blast_tac 1);
-qed "bex_image";
-
-Addsimps [ball_image,bex_image];
-
 (*** Range of a function -- just a translation for image! ***)
 
 goal thy "!!b. b=f(x) ==> b : range(f)";