src/HOL/Deriv.thy
 changeset 41368 8afa26855137 parent 37891 c26f9d06e82c child 41550 efa734d9b221
```--- 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)"