Replaced Suc(Suc 0) by 2; it improves readability a little

--- a/src/HOL/ex/NatSum.ML	Thu Aug 21 12:53:23 1997 +0200
+++ b/src/HOL/ex/NatSum.ML	Thu Aug 21 12:54:20 1997 +0200
@@ -19,7 +19,7 @@
 qed "sum_of_naturals";
 
 goal NatSum.thy
-  "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
+  "Suc(Suc(Suc(Suc 2)))*sum (%i.i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
 by (Simp_tac 1);
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);
@@ -27,7 +27,7 @@
 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)";
+  "Suc(Suc 2)*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
 by (Simp_tac 1);
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);