src/HOL/Multivariate_Analysis/Integration.thy
changeset 44140 2c10c35dd4be
parent 44125 230a8665c919
child 44167 e81d676d598e
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 10 15:56:48 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 10 16:35:50 2011 -0700
     1.3 @@ -3763,8 +3763,9 @@
     1.4        using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
     1.5      have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
     1.6        apply(rule diff_chain_within) apply(rule has_derivative_add)
     1.7 -      unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
     1.8 -      apply(rule has_derivative_vmul_within,rule has_derivative_id)+ 
     1.9 +      unfolding scaleR_simps
    1.10 +      apply(intro has_derivative_intros)
    1.11 +      apply(intro has_derivative_intros)
    1.12        apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
    1.13        apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
    1.14      thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .