# HG changeset patch
# User haftmann
# Date 1263540441 -3600
# Node ID bb9dad7de5151a7a057812628a4efb88fc1a387e
# Parent  a64c7228e6602fa3fb1d5a1313f5f7b365df1b48
spurious proof failure

diff -r a64c7228e660 -r bb9dad7de515 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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. *}