# HG changeset patch
# User paulson
# Date 834748641 -7200
# Node ID 10494d0241cd68ead119d3b8f9d4e2f1177182ee
# Parent  cfa0052d5fe9b48a22f45160ce3b4859ca03cd4c
Explicitly included add_mult_distrib & add_mult_distrib2

diff -r cfa0052d5fe9 -r 10494d0241cd src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Fri Jun 14 12:34:56 1996 +0200
+++ b/src/HOL/ex/NatSum.ML	Fri Jun 14 12:37:21 1996 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/natsum.ML
+(*  Title:      HOL/ex/NatSum.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
@@ -7,6 +7,7 @@
 *)
 
 Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
+Addsimps [add_mult_distrib,add_mult_distrib2];
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
 goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
@@ -17,8 +18,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(Suc(Suc(0))*n)";
+  "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*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);