--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sat Aug 27 17:26:14 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Aug 28 09:20:12 2011 -0700
@@ -47,7 +47,7 @@
shows "FDERIV f x :> f' = (f has_derivative f') (at x)"
unfolding fderiv_def has_derivative_def netlimit_at_vector
by (simp add: diff_diff_eq Lim_at_zero [where a=x]
- LIM_norm_zero_iff [where 'b='b, symmetric])
+ tendsto_norm_zero_iff [where 'b='b, symmetric])
lemma DERIV_conv_has_derivative:
"(DERIV f x :> f') = (f has_derivative op * f') (at x)"