# HG changeset patch
# User desharna
# Date 1672059247 -3600
# Node ID b61ad889dffa6b8920e18337862031d7e6b2cf94
# Parent  907b5c4d13321a1cac6d6435d3f4ad4731cbc162
removed old lemma names

diff -r 907b5c4d1332 -r b61ad889dffa src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Dec 23 12:14:10 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 26 13:54:07 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>