src/HOL/Multivariate_Analysis/Derivative.thy

   shows "\<exists>x\<in>{a<..<b}. (f b - f a = (f' x) (b - a))"
 proof-
   have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
     apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
     defer
-    apply(rule continuous_on_intros assms(2) continuous_on_cmul[where 'b=real, unfolded real_scaleR_def])+
+    apply(rule continuous_on_intros assms(2))+
   proof
     fix x assume x:"x \<in> {a<..<b}"
     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
       by (intro has_derivative_intros assms(3)[rule_format,OF x]
         mult_right_has_derivative)

   have *:"\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
     using assms(1)[unfolded convex_alt,rule_format,OF x y]
     unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
     by (auto simp add: algebra_simps)
   hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply-
-    apply(rule continuous_on_intros continuous_on_vmul)+
+    apply(rule continuous_on_intros)+
     unfolding continuous_on_eq_continuous_within
     apply(rule,rule differentiable_imp_continuous_within)
     unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
     apply(rule has_derivative_within_subset)
     apply(rule assms(2)[rule_format]) by auto