--- a/NEWS Thu Dec 08 13:53:28 2011 +0100
+++ b/NEWS Fri Dec 09 11:31:13 2011 +0100
@@ -137,6 +137,10 @@
zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
zero_le_zpower_abs ~> zero_le_power_abs
+* Theory Deriv: Renamed
+
+ DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
+
* New "case_product" attribute to generate a case rule doing multiple
case distinctions at the same time. E.g.
--- a/src/HOL/Deriv.thy Thu Dec 08 13:53:28 2011 +0100
+++ b/src/HOL/Deriv.thy Fri Dec 09 11:31:13 2011 +0100
@@ -1223,7 +1223,7 @@
by (metis DERIV_unique less_le)
qed
-lemma DERIV_nonneg_imp_nonincreasing:
+lemma DERIV_nonneg_imp_nondecreasing:
fixes a::real and b::real and f::"real => real"
assumes "a \<le> b" and
"\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<ge> 0)"
@@ -1275,7 +1275,7 @@
shows "f a \<ge> f b"
proof -
have "(%x. -f x) a \<le> (%x. -f x) b"
- apply (rule DERIV_nonneg_imp_nonincreasing [of a b "%x. -f x"])
+ apply (rule DERIV_nonneg_imp_nondecreasing [of a b "%x. -f x"])
using assms
apply auto
apply (metis DERIV_minus neg_0_le_iff_le)