src/HOL/Multivariate_Analysis/Derivative.thy

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Nov 01 18:51:14 2013 +0100
@@ -516,7 +516,7 @@
       unfolding e_def
       using c[THEN conjunct1]
       using norm_minus_cancel[of "f' i - f'' i"]
-      by (auto simp add: add.commute ab_diff_minus)
+      by auto
     finally show False
       using c
       using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R i"]