--- a/src/HOL/Relation.thy Mon Dec 26 19:07:42 2022 +0100
+++ b/src/HOL/Relation.thy Mon Dec 26 19:13:37 2022 +0100
@@ -727,23 +727,15 @@
lemma (in preorder) transp_on_le[simp]: "transp_on A (\<le>)"
by (auto intro: transp_onI order_trans)
-lemmas (in preorder) transp_le = transp_on_le[of UNIV]
-
lemma (in preorder) transp_on_less[simp]: "transp_on A (<)"
by (auto intro: transp_onI less_trans)
-lemmas (in preorder) transp_less = transp_on_less[of UNIV]
-
lemma (in preorder) transp_on_ge[simp]: "transp_on A (\<ge>)"
by (auto intro: transp_onI order_trans)
-lemmas (in preorder) transp_ge = transp_on_ge[of UNIV]
-
lemma (in preorder) transp_on_greater[simp]: "transp_on A (>)"
by (auto intro: transp_onI less_trans)
-lemmas (in preorder) transp_gr = transp_on_greater[of UNIV]
-
subsubsection \<open>Totality\<close>