src/HOL/ex/NatSum.thy

--- a/src/HOL/ex/NatSum.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/ex/NatSum.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -106,7 +106,7 @@
   "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
     of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
     (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
-  by (induct m) simp_all
+  by (induct m) (simp_all add: of_nat_mult)
 
 
 text {*