diff -r fa63bde6d659 -r 39a311f50344 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Sun May 20 20:14:30 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Sun May 20 22:10:21 2018 +0100
@@ -638,21 +638,21 @@
 lemma mvt_simple:
   fixes f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
   shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
 proof (rule mvt)
   have "f differentiable_on {a..b}"
-    by (meson atLeastAtMost_iff derf differentiable_at_imp_differentiable_on differentiable_def)
+    using derf unfolding differentiable_on_def differentiable_def by force
   then show "continuous_on {a..b} f"
     by (rule differentiable_imp_continuous_on)
   show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
-    by (metis derf not_less order.asym that)
+    by (metis at_within_Icc_at derf leI order.asym that)
 qed (rule assms)
 
 lemma mvt_very_simple:
   fixes f :: "real \<Rightarrow> real"
   assumes "a \<le> b"
-    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
   shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
 proof (cases "a = b")
   interpret bounded_linear "f' b"
@@ -2822,8 +2822,7 @@
     (if x \<in> S then f' x else g' x)) (at x within u)"
   unfolding has_vector_derivative_def assms
   using x_in
-  apply (intro has_derivative_If_within_closures[where
-        ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
+  apply (intro has_derivative_If_within_closures[where ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
         THEN has_derivative_eq_rhs])
   subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
   subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)