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