# HG changeset patch
# User paulson
# Date 953304673 -3600
# Node ID 60c2f892b1d9a3aa18d12dff90be208410628ac9
# Parent  6343c725ba7e05b8d10558ce779d9a974e68adf7
re-ordered the theorems

diff -r 6343c725ba7e -r 60c2f892b1d9 src/HOL/ex/NatSum.ML
--- 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";
-