src/HOL/Library/Complete_Partial_Order2.thy

--- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Oct 27 21:38:41 2019 -0400
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Mon Oct 28 18:50:40 2019 +0000
@@ -417,8 +417,7 @@
 
 context preorder begin
 
-lemma transp_le [simp, cont_intro]: "transp (\<le>)"
-by(rule transpI)(rule order_trans)
+declare transp_le[cont_intro]
 
 lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)"
 by(rule monotoneI) simp