author | Peter Lammich |
Mon, 28 Oct 2019 18:50:40 +0000 | |
changeset 70961 | 70fb697be418 |
parent 70960 | 84f79d82df0a |
child 70963 | bbe5fe8bba71 |
--- 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