diff -r 2cd0dd4de9c3 -r b98f1057da0e src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Aug 06 18:14:45 2024 +0100
+++ b/src/HOL/Deriv.thy	Tue Aug 06 22:47:44 2024 +0100
@@ -1960,10 +1960,10 @@
 qed
 
 
-proposition  deriv_nonneg_imp_mono: (*DELETE*)
-  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
-  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
-  assumes ab: "a \<le> b"
+proposition deriv_nonneg_imp_mono: 
+  assumes "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes "a \<le> b"
   shows "g a \<le> g b"
   by (metis DERIV_nonneg_imp_nondecreasing atLeastAtMost_iff assms)