New rewrite rules for quantification over bounded UNIONs

--- a/src/HOL/equalities.ML	Fri Jul 31 18:46:55 1998 +0200
+++ b/src/HOL/equalities.ML	Mon Aug 03 10:36:39 1998 +0200
@@ -767,6 +767,7 @@
      "(ALL x:UNIV. P x) = (ALL x. P x)",
      "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
      "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
+     "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
      "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
      "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
      "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
@@ -781,6 +782,7 @@
      "(EX x:UNIV. P x) = (EX x. P x)",
      "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
      "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
+     "(EX x: UNION A B. P x) = (EX a:A. EX x: B a.  P x)",
      "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
      "(EX x:f``A. P x) = (EX x:A. P(f x))",
      "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];