src/ZF/equalities.ML
changeset 182 e30b55c07235
parent 0 a5a9c433f639
child 192 3dc5c8016a0e
equal deleted inserted replaced
181:9c2db771f224 182:e30b55c07235
   237 by (fast_tac eq_cs 1);
   237 by (fast_tac eq_cs 1);
   238 val Diff_INT = result();
   238 val Diff_INT = result();
   239 
   239 
   240 (** Unions and Intersections with General Sum **)
   240 (** Unions and Intersections with General Sum **)
   241 
   241 
       
   242 goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
       
   243 by (fast_tac eq_cs 1);
       
   244 val SUM_UN_distrib1 = result();
       
   245 
       
   246 goal ZF.thy "(SUM x:A. UN y:B. C(x,y)) = (UN y:B. SUM x:A. C(x,y))";
       
   247 by (fast_tac eq_cs 1);
       
   248 val SUM_UN_distrib2 = result();
       
   249 
   242 goal ZF.thy "(SUM x:A Un B. C(x)) = (SUM x:A. C(x)) Un (SUM x:B. C(x))";
   250 goal ZF.thy "(SUM x:A Un B. C(x)) = (SUM x:A. C(x)) Un (SUM x:B. C(x))";
   243 by (fast_tac eq_cs 1);
   251 by (fast_tac eq_cs 1);
   244 val SUM_Un_distrib1 = result();
   252 val SUM_Un_distrib1 = result();
   245 
   253 
   246 goal ZF.thy
   254 goal ZF.thy