src/HOL/Sum.ML
changeset 3091 9366415b93ad
parent 2922 580647a879cf
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/Sum.ML	Thu May 01 10:28:10 1997 +0200
     1.2 +++ b/src/HOL/Sum.ML	Fri May 02 10:17:44 1997 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  qed "sum_case_Inl";
     1.5  
     1.6  goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
     1.7 -by (fast_tac (!claset addIs [select_equality]) 1);
     1.8 +by (blast_tac (!claset addIs [select_equality]) 1);
     1.9  qed "sum_case_Inr";
    1.10  
    1.11  Addsimps [sum_case_Inl, sum_case_Inr];