src/HOL/Transcendental.thy
changeset 57418 6ab1c7cb0b8d
parent 57275 0ddb5b755cdc
child 57492 74bf65a1910a
     1.1 --- a/src/HOL/Transcendental.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -237,7 +237,7 @@
     1.4      have "?s sums y" using sums_if'[OF `f sums y`] .
     1.5      from this[unfolded sums_def, THEN LIMSEQ_Suc]
     1.6      have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
     1.7 -      by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum_reindex if_eq sums_def cong del: if_cong)
     1.8 +      by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong)
     1.9    }
    1.10    from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
    1.11  qed
    1.12 @@ -478,7 +478,7 @@
    1.13    apply (subst sumr_diff_mult_const2)
    1.14    apply simp
    1.15    apply (simp only: lemma_termdiff1 setsum_right_distrib)
    1.16 -  apply (rule setsum_cong [OF refl])
    1.17 +  apply (rule setsum.cong [OF refl])
    1.18    apply (simp add: less_iff_Suc_add)
    1.19    apply (clarify)
    1.20    apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
    1.21 @@ -1071,7 +1071,7 @@
    1.22    also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
    1.23               (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
    1.24               (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.25 -    by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
    1.26 +    by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric]
    1.27                     real_of_nat_add [symmetric]) simp
    1.28    also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
    1.29      by (simp only: scaleR_right.setsum)