diff -r 9c2db771f224 -r e30b55c07235 src/ZF/equalities.ML --- 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();