# HG changeset patch
# User paulson
# Date 833794886 -7200
# Node ID 173ce86b4c22fc31de778f98a4aaff6cdabc1ba8
# Parent  ab45b881fa62c85dacc26249e5d6780e97a8e39e
Used 2 instead of Suc(Suc 0)

diff -r ab45b881fa62 -r 173ce86b4c22 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Mon Jun 03 11:41:00 1996 +0200
+++ b/src/HOL/ex/NatSum.ML	Mon Jun 03 11:41:26 1996 +0200
@@ -9,7 +9,7 @@
 Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
-goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)";
+goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
 by (Simp_tac 1);
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);