src/HOL/MacLaurin.thy
changeset 63365 5340fb6633d0
parent 63040 eb4ddd18d635
child 63569 7e0b0db5e9ac
     1.1 --- a/src/HOL/MacLaurin.thy	Sat Jul 02 08:41:05 2016 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Sat Jul 02 08:41:05 2016 +0200
     1.3 @@ -50,7 +50,8 @@
     1.4      unfolding atLeast0LessThan[symmetric] by auto
     1.5    have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) =
     1.6        (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)))"
     1.7 -    unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
     1.8 +    unfolding intvl
     1.9 +    by (subst setsum.insert) (auto simp add: setsum.reindex)
    1.10    moreover
    1.11    have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
    1.12      by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff)