src/HOL/Sum.ML
changeset 1761 29e08d527ba1
parent 1760 6f41a494f3b1
child 1985 84cf16192e03
     1.1 --- a/src/HOL/Sum.ML	Thu May 23 14:37:06 1996 +0200
     1.2 +++ b/src/HOL/Sum.ML	Thu May 23 15:15:20 1996 +0200
     1.3 @@ -204,14 +204,14 @@
     1.4  qed "PartD1";
     1.5  
     1.6  goal Sum.thy "Part A (%x.x) = A";
     1.7 -by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
     1.8 +by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
     1.9  qed "Part_id";
    1.10  
    1.11  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
    1.12 -by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    1.13 +by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
    1.14  qed "Part_Int";
    1.15  
    1.16  (*For inductive definitions*)
    1.17  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
    1.18 -by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    1.19 +by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
    1.20  qed "Part_Collect";