--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Apr 06 17:19:08 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Apr 06 21:01:33 2014 +0200
@@ -127,7 +127,7 @@
"(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
proof -
have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
- by (metis divide_diff_eq_iff eq_iff_diff_eq_0)
+ by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult_commute)
show ?thesis
apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
apply (simp add: LIM_zero_iff [where l = D, symmetric])