Removed dup lemma that inhibited locale instantiations (dup fact error)
authorPeter Lammich
Mon, 28 Oct 2019 18:50:40 +0000
changeset 70961 70fb697be418
parent 70960 84f79d82df0a
child 70963 bbe5fe8bba71
Removed dup lemma that inhibited locale instantiations (dup fact error)
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