1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Feb 17 17:57:37 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Feb 17 18:33:45 2010 +0100
     1.3 @@ -387,7 +387,7 @@
     1.4        apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed
     1.5  
     1.6  lemma has_derivative_at_alt:
     1.7 -  "(f has_derivative f') (at (x::real^'n)) \<longleftrightarrow> bounded_linear f' \<and>
     1.8 +  "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
     1.9    (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm(f y - f x - f'(y - x)) \<le> e * norm(y - x))"
    1.10    using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto
    1.11