src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 67968 a5ad4c015d1c
parent 67399 eab6ce8368fa
child 67979 53323937ee25
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Apr 09 16:20:23 2018 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4    "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
     1.5    by (metis DERIV_zero_unique UNIV_I convex_UNIV)
     1.6  
     1.7 -subsection \<open>Some limit theorems about real part of real series etc.\<close>
     1.8 +subsection \<open>Some limit theorems about real part of real series etc\<close>
     1.9  
    1.10  (*MOVE? But not to Finite_Cartesian_Product*)
    1.11  lemma sums_vec_nth :