# HG changeset patch
# User Peter Lammich
# Date 1572288640 0
# Node ID 70fb697be418850f4d59c70fd4a0b74df1d0cf29
# Parent  84f79d82df0a855e0fd39bd09121da28320c9836
Removed dup lemma that inhibited locale instantiations (dup fact error)

diff -r 84f79d82df0a -r 70fb697be418 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