# HG changeset patch
# User paulson
# Date 958137646 -7200
# Node ID 9ba7ef8a765ba0d261dd488ba527cf0f6768f0f2
# Parent  851693e780d65afd10c3aeae232fce6f7dc96b86
new simprules needed because of new subtraction rewriting

diff -r 851693e780d6 -r 9ba7ef8a765b src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Fri May 12 15:18:55 2000 +0200
+++ b/src/HOL/ex/NatSum.ML	Fri May 12 15:20:46 2000 +0200
@@ -13,6 +13,7 @@
 *)
 
 Addsimps [add_mult_distrib, add_mult_distrib2];
+Addsimps [diff_mult_distrib, diff_mult_distrib2];
 
 (*The sum of the first n odd numbers equals n squared.*)
 Goal "sum (%i. Suc(i+i)) n = n*n";