Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Mon, 28 Oct 2019 20:00:36 +0100
changeset 70963 bbe5fe8bba71
parent 70961 70fb697be418 (diff)
parent 70962 e8207714d505 (current diff)
child 70964 99eec58dc551
merged
src/HOL/Analysis/metricarith.ml file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Mon Oct 28 19:52:57 2019 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Mon Oct 28 20:00:36 2019 +0100
@@ -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
isabelle