Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Complete_Partial_Order2.thy
changeset 69038 2ce9bc515a64
parent 68980 5717fbc55521
child 69039 51005671bee5 
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Sep 23 13:45:37 2018 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Sun Sep 23 15:42:19 2018 +0200
@@ -161,7 +161,7 @@
 end
 
 lemma Sup_image_mono_le:
-  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or> _" [900] 900)
+  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>")
   assumes ccpo: "class.ccpo Sup_b (\<sqsubseteq>) lt_b"
   assumes chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
   and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
isabelle