# HG changeset patch
# User paulson
# Date 872160860 -7200
# Node ID bc2c363371ee27a6a4a1aaadc10ebd7016de8d67
# Parent  a64c8fbcd98f8149b762eb7ba5bfc1d0dc1a0aac
Replaced Suc(Suc 0) by 2; it improves readability a little

diff -r a64c8fbcd98f -r bc2c363371ee src/HOL/ex/NatSum.ML
--- 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);