1.1 --- a/src/HOL/Algebra/abstract/NatSum.ML Thu Nov 11 10:25:17 1999 +0100
1.2 +++ b/src/HOL/Algebra/abstract/NatSum.ML Thu Nov 11 10:25:29 1999 +0100
1.3 @@ -4,8 +4,6 @@
1.4 Author: Clemens Ballarin, started 12 December 1996
1.5 *)
1.6
1.7 -open NatSum;
1.8 -
1.9 section "Basic Properties";
1.10
1.11 Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";
1.12 @@ -164,12 +162,12 @@
1.13 \ SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
1.14 by (nat_ind_tac "n" 1);
1.15 (* Base case *)
1.16 -by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
1.17 +by (Simp_tac 1);
1.18 (* Induction step *)
1.19 -by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
1.20 +by (Asm_simp_tac 1);
1.21 by (Clarify_tac 1);
1.22 by (res_inst_tac [("f", "f")] arg_cong 1);
1.23 -by (fast_arith_tac 1);
1.24 +by (arith_tac 1);
1.25 qed "SUM_if_singleton";
1.26
1.27 Goal