# HG changeset patch
# User desharna
# Date 1672059846 -3600
# Node ID 2735b11a3de8ec02cf9b9f0b38725ec5433eb131
# Parent  602ddfb744b1a5f4bb889f97828e0bf759eb30d4# Parent  b61ad889dffa6b8920e18337862031d7e6b2cf94
merged

diff -r 602ddfb744b1 -r 2735b11a3de8 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Dec 24 15:35:43 2022 +0000
+++ b/src/HOL/Relation.thy	Mon Dec 26 14:04:06 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>