# HG changeset patch
# User nipkow
# Date 879595852 -3600
# Node ID 551684f275b974925b150e4e3d980fb0c4058381
# Parent  22e3f0368c85eef4151332737bcd170deee469d6
Added

> "(? x : f `` A. P x) = (? a:A. P(f a))"
> "(! x : f `` A. P x) = (! a:A. P(f a))"

diff -r 22e3f0368c85 -r 551684f275b9 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Nov 14 15:51:09 1997 +0100
+++ b/src/HOL/Set.ML	Sat Nov 15 13:10:52 1997 +0100
@@ -610,6 +610,16 @@
 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)";