--- a/src/HOL/Hyperreal/Transcendental.thy Wed May 30 01:53:38 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed May 30 02:41:26 2007 +0200
@@ -720,7 +720,7 @@
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
real_of_nat_add [symmetric], simp)
also have "\<dots> = real (Suc n) *# (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
- by (simp only: additive_scaleR_right.setsum)
+ by (simp only: scaleR_right.setsum)
finally show
"S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc)