--- a/src/HOL/equalities.ML Thu Apr 02 13:48:48 1998 +0200
+++ b/src/HOL/equalities.ML Thu Apr 02 13:49:04 1998 +0200
@@ -465,6 +465,10 @@
by (Blast_tac 1);
qed "UN_Un";
+goal thy "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)";
+by (Blast_tac 1);
+qed "UN_UN_flatten";
+
goal thy "(INT x:insert a A. B x) = B a Int INTER A B";
by (Blast_tac 1);
qed "INT_insert";
@@ -574,6 +578,14 @@
by (Blast_tac 1);
qed "bex_Un";
+goal thy "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)";
+by (Blast_tac 1);
+qed "ball_UN";
+
+goal thy "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)";
+by (Blast_tac 1);
+qed "bex_UN";
+
section "-";