src/HOL/Multivariate_Analysis/Derivative.thy

   using assms(4-5)
   unfolding sums_def
   apply auto
   done
 
-text \<open>Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector.\<close>
+text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
 
 definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
 
 lemma vector_derivative_unique_at:
   assumes "(f has_vector_derivative f') (at x)"