--- a/src/HOL/ex/NatSum.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/ex/NatSum.ML Mon Jun 22 17:26:46 1998 +0200
@@ -12,14 +12,14 @@
Addsimps [add_mult_distrib, add_mult_distrib2];
(*The sum of the first n positive integers equals n(n+1)/2.*)
-goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";
+Goal "2*sum (%i. i) (Suc n) = n*Suc(n)";
by (Simp_tac 1);
by (induct_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "sum_of_naturals";
-goal NatSum.thy
+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);
@@ -27,7 +27,7 @@
by (Asm_simp_tac 1);
qed "sum_of_squares";
-goal NatSum.thy
+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);
@@ -36,7 +36,7 @@
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";
+Goal "sum (%i. Suc(i+i)) n = n*n";
by (induct_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);