src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

   assumes "convex s" shows "convex(closure s)"
   unfolding convex_def Ball_def closure_sequential
   apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
   apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
   apply(rule assms[unfolded convex_def, rule_format]) prefer 6
-  apply(rule Lim_add) apply(rule_tac [1-2] Lim_cmul) by auto
+  by (auto intro: tendsto_intros)
 
 lemma convex_interior:
   fixes s :: "'a::real_normed_vector set"
   assumes "convex s" shows "convex(interior s)"
   unfolding convex_alt Ball_def mem_interior apply(rule,rule,rule,rule,rule,rule) apply(erule exE | erule conjE)+ proof-