--- a/src/HOL/ex/NatSum.ML Wed Oct 04 13:11:57 1995 +0100
+++ b/src/HOL/ex/NatSum.ML Wed Oct 04 13:12:14 1995 +0100
@@ -6,38 +6,37 @@
Summing natural numbers, squares and cubes. Could be continued...
*)
-val natsum_ss = arith_ss addsimps
- ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
+Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
(*The sum of the first n positive integers equals n(n+1)/2.*)
goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)";
-by (simp_tac natsum_ss 1);
+by (Simp_tac 1);
by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "sum_of_naturals";
goal NatSum.thy
"Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = \
\ n*Suc(n)*Suc(Suc(Suc(0))*n)";
-by (simp_tac natsum_ss 1);
+by (Simp_tac 1);
by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "sum_of_squares";
goal NatSum.thy
"Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
-by (simp_tac natsum_ss 1);
+by (Simp_tac 1);
by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "sum_of_cubes";
(*The sum of the first n odd numbers equals n squared.*)
goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n";
by (nat_ind_tac "n" 1);
-by (simp_tac natsum_ss 1);
-by (asm_simp_tac natsum_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "sum_of_odds";