1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 13 12:51:52 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 13 13:31:26 2012 +0100
     1.3 @@ -1689,7 +1689,7 @@
     1.4  proof
     1.5    assume ?l guess f' using `?l`[unfolded differentiable_def] .. note f' = this
     1.6    then interpret bounded_linear f' by auto
     1.7 -  thus ?r unfolding vector_derivative_def has_vector_derivative_def
     1.8 +  show ?r unfolding vector_derivative_def has_vector_derivative_def
     1.9      apply-apply(rule someI_ex,rule_tac x="f' 1" in exI)
    1.10      using f' unfolding scaleR[THEN sym] by auto
    1.11  next