diff -r d32201f08e98 -r 6fb4a0829cc4 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Jun 20 11:06:33 2022 +0200
+++ b/src/HOL/Orderings.thy	Tue Jun 21 13:39:06 2022 +0200
@@ -1060,15 +1060,6 @@
 
 subsection \<open>Monotonicity\<close>
 
-definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-  where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
-
-lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
-  unfolding monotone_def by iprover
-
-lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
-  unfolding monotone_def by iprover
-
 context order
 begin