--- a/src/ZF/equalities.ML Thu Dec 02 12:49:03 1993 +0100
+++ b/src/ZF/equalities.ML Fri Dec 03 12:47:45 1993 +0100
@@ -239,6 +239,14 @@
(** Unions and Intersections with General Sum **)
+goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
+by (fast_tac eq_cs 1);
+val SUM_UN_distrib1 = result();
+
+goal ZF.thy "(SUM x:A. UN y:B. C(x,y)) = (UN y:B. SUM x:A. C(x,y))";
+by (fast_tac eq_cs 1);
+val SUM_UN_distrib2 = result();
+
goal ZF.thy "(SUM x:A Un B. C(x)) = (SUM x:A. C(x)) Un (SUM x:B. C(x))";
by (fast_tac eq_cs 1);
val SUM_Un_distrib1 = result();