src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 61518 ff12606337e9
parent 61426 d53db136e8fd
child 61524 f2e51e704a96
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Oct 25 17:31:14 2015 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Oct 26 23:41:27 2015 +0000
     1.3 @@ -464,7 +464,7 @@
     1.4    "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
     1.5  proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
     1.6    show "convex (closed_segment 0 z)"
     1.7 -    by (rule convex_segment [of 0 z])
     1.8 +    by (rule convex_closed_segment [of 0 z])
     1.9  next
    1.10    fix k x
    1.11    assume "x \<in> closed_segment 0 z" "k \<le> n"