# HG changeset patch
# User paulson
# Date 952529086 -3600
# Node ID 14d89313c66c3fae4db525abf8b00ea342615b9e
# Parent  04d0f732e24ea9a51de188213f373c6e8619c33c
tidied

diff -r 04d0f732e24e -r 14d89313c66c src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Wed Mar 08 16:17:10 2000 +0100
+++ b/src/HOL/ex/NatSum.ML	Wed Mar 08 16:24:46 2000 +0100
@@ -7,30 +7,23 @@
 Demonstrates permutative rewriting.
 *)
 
-Delsimprocs nat_cancel;
 Addsimps add_ac;
 Addsimps [add_mult_distrib, add_mult_distrib2];
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
-Goal "2*sum (%i. i) (Suc n) = n*Suc(n)";
-by (Simp_tac 1);
+Goal "2 * sum id (Suc n) = n*Suc(n)";
 by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
 qed "sum_of_naturals";
 
 Goal "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
-by (Simp_tac 1);
 by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
 qed "sum_of_squares";
 
 Goal "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
-by (Simp_tac 1);
 by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
 qed "sum_of_cubes";
 
 (*The sum of the first n odd numbers equals n squared.*)
diff -r 04d0f732e24e -r 14d89313c66c src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Wed Mar 08 16:17:10 2000 +0100
+++ b/src/HOL/ex/NatSum.thy	Wed Mar 08 16:24:46 2000 +0100
@@ -6,7 +6,7 @@
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
 *)
 
-NatSum = Arith +
+NatSum = Main +
 consts sum     :: [nat=>nat, nat] => nat
 primrec 
   "sum f 0 = 0"