src/HOL/Sum.ML
changeset 2922 580647a879cf
parent 2891 d8f254ad1ab9
child 3091 9366415b93ad
     1.1 --- a/src/HOL/Sum.ML	Wed Apr 09 12:31:11 1997 +0200
     1.2 +++ b/src/HOL/Sum.ML	Wed Apr 09 12:32:04 1997 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4  qed "Part_subset";
     1.5  
     1.6  goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
     1.7 -by (Fast_tac 1);
     1.8 +by (Blast_tac 1);
     1.9  qed "Part_mono";
    1.10  
    1.11  val basic_monos = basic_monos @ [Part_mono];
    1.12 @@ -199,10 +199,10 @@
    1.13  qed "Part_id";
    1.14  
    1.15  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
    1.16 -by (Fast_tac 1);
    1.17 +by (Blast_tac 1);
    1.18  qed "Part_Int";
    1.19  
    1.20  (*For inductive definitions*)
    1.21  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
    1.22 -by (Fast_tac 1);
    1.23 +by (Blast_tac 1);
    1.24  qed "Part_Collect";