# HG changeset patch
# User nipkow
# Date 879693511 -3600
# Node ID a73f5a63f197c94f30d2fd51179c6f3b9bee025a
# Parent  eb5586526bc9a5f02575f5129e1895929cf943c8
Removed
     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
     "(EX x:f``A. P x) = (EX x:A. P(f x))",
again, because they were already there and added
"(UN x:f``A. B x)     = (UN a:A. B(f a))"
"(INT x:f``A. B x)    = (INT a:A. B(f a))"
instead.

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)";
diff -r eb5586526bc9 -r a73f5a63f197 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Sat Nov 15 18:41:06 1997 +0100
+++ b/src/HOL/equalities.ML	Sun Nov 16 16:18:31 1997 +0100
@@ -626,7 +626,8 @@
      "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
      "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
      "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
-     "(UN x:C. A - B x)    = (A - (INT x:C. B x))"];
+     "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
+     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
 
 val INT_simps = map prover
     ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
@@ -635,7 +636,8 @@
      "!!C. C ~= {} ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
      "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
      "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
-     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))"];
+     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
+     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
 
 
 val ball_simps = map prover