--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jan 14 18:44:22 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 15 08:27:21 2010 +0100
@@ -607,7 +607,8 @@
have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"])
using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
- unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding group_simps by auto qed
+ unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding group_simps by (auto intro: mult_pos_pos)
+qed
subsection {* In particular if we have a mapping into R^1. *}