# HG changeset patch
# User hoelzl
# Date 1292940059 -3600
# Node ID 8afa2685513763a74266b7dd628ce86f0e48e26e
# Parent  1b65137d598c2a08a1fb0d9a802724f4a1a029c3
use DERIV_intros

diff -r 1b65137d598c -r 8afa26855137 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Dec 21 14:50:53 2010 +0100
+++ b/src/HOL/Deriv.thy	Tue Dec 21 15:00:59 2010 +0100
@@ -879,14 +879,14 @@
   fixes f :: "real => real"
   shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
   apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
-  apply (auto simp add: DERIV_minus) 
+  apply (auto simp add: DERIV_minus)
   done
 
 lemma DERIV_neg_dec_right:
   fixes f :: "real => real"
   shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
   apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
-  apply (auto simp add: DERIV_minus) 
+  apply (auto simp add: DERIV_minus)
   done
 
 lemma DERIV_local_max:
@@ -1554,21 +1554,8 @@
   then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
 
   from cdef have "DERIV ?h c :> l" by auto
-  moreover
-  {
-    have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
-      apply (insert DERIV_const [where k="f b - f a"])
-      apply (drule meta_spec [of _ c])
-      apply (drule DERIV_mult [OF _ g'cdef])
-      by simp
-    moreover have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
-      apply (insert DERIV_const [where k="g b - g a"])
-      apply (drule meta_spec [of _ c])
-      apply (drule DERIV_mult [OF _ f'cdef])
-      by simp
-    ultimately have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
-      by (simp add: DERIV_diff)
-  }
+  moreover have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
+    using g'cdef f'cdef by (auto intro!: DERIV_intros)
   ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
 
   {