# HG changeset patch
# User noschinl
# Date 1323426673 -3600
# Node ID d985ec9748156b1b8009bacb1392f11dead86db2
# Parent  3355c27c93a474bf27acdeb6d9e708c9e01bf615
more systematic lemma name

diff -r 3355c27c93a4 -r d985ec974815 NEWS
--- 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.
 
diff -r 3355c27c93a4 -r d985ec974815 src/HOL/Deriv.thy
--- 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)