# HG changeset patch # User paulson # Date 1526850621 -3600 # Node ID 39a311f50344608ac8abca2a8b57cea4b02aa31f # Parent fa63bde6d65965e0a2de651b7f7a7e53850d0c76 correcting the statements of the MVTs 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 \ real" assumes "a < b" - and derf: "\x. \a \ x; x \ b\ \ (f has_derivative f' x) (at x)" + and derf: "\x. \a \ x; x \ b\ \ (f has_derivative f' x) (at x within {a..b})" shows "\x\{a<.. real" assumes "a \ b" - and derf: "\x. \a \ x; x \ b\ \ (f has_derivative f' x) (at x)" + and derf: "\x. \a \ x; x \ b\ \ (f has_derivative f' x) (at x within {a..b})" shows "\x\{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 \ 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' = "\x a. a *\<^sub>R f' x" and ?g' = "\x a. a *\<^sub>R g' x", + apply (intro has_derivative_If_within_closures[where ?f' = "\x a. a *\<^sub>R f' x" and ?g' = "\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)