--- a/src/HOL/ex/NatSum.ML Fri Mar 17 15:49:50 2000 +0100
+++ b/src/HOL/ex/NatSum.ML Fri Mar 17 15:51:13 2000 +0100
@@ -9,7 +9,11 @@
thanks to new simprocs.
*)
-Addsimps [add_mult_distrib, add_mult_distrib2];
+(*The sum of the first n odd numbers equals n squared.*)
+Goal "sum (%i. Suc(i+i)) n = n*n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sum_of_odds";
(*The sum of the first n positive integers equals n(n+1)/2.*)
Goal "2 * sum id (Suc n) = n*Suc(n)";
@@ -17,6 +21,8 @@
by Auto_tac;
qed "sum_of_naturals";
+Addsimps [add_mult_distrib, add_mult_distrib2];
+
Goal "Suc(Suc(Suc(Suc 2))) * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(2*n)";
by (induct_tac "n" 1);
by Auto_tac;
@@ -26,10 +32,3 @@
by (induct_tac "n" 1);
by Auto_tac;
qed "sum_of_cubes";
-
-(*The sum of the first n odd numbers equals n squared.*)
-Goal "sum (%i. Suc(i+i)) n = n*n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_odds";
-