src/HOL/Sum.ML
changeset 1188 0443e4dc8511
parent 923 ff1574a81019
child 1264 3eb91524b938
     1.1 --- a/src/HOL/Sum.ML	Tue Jul 25 16:58:06 1995 +0200
     1.2 +++ b/src/HOL/Sum.ML	Tue Jul 25 16:59:08 1995 +0200
     1.3 @@ -202,3 +202,11 @@
     1.4  by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
     1.5  qed "Part_id";
     1.6  
     1.7 +goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
     1.8 +by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
     1.9 +qed "Part_Int";
    1.10 +
    1.11 +(*For inductive definitions*)
    1.12 +goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
    1.13 +by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
    1.14 +qed "Part_Collect";