# 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);