# 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 (\)" 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 (\)" 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 \Totality\