# HG changeset patch
# User nipkow
# Date 1537715646 -7200
# Node ID 51005671bee545e54adcdddddc9335ec0ebc0733
# Parent  2ce9bc515a64151b0d0fb86197682b7be7f3bca3
More standard precedences

diff -r 2ce9bc515a64 -r 51005671bee5 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Sep 23 15:42:19 2018 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Sun Sep 23 17:14:06 2018 +0200
@@ -556,7 +556,7 @@
 
 context
   fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
-  and lub :: "'b set \<Rightarrow> 'b" ("\<Or> _" [900] 900)
+  and lub :: "'b set \<Rightarrow> 'b" ("\<Or>")
 begin
 
 lemma cont_fun_lub_Sup:
@@ -677,7 +677,7 @@
 by(rule monotoneI)(auto intro: bot intro: mono order_trans)
 
 lemma (in ccpo) mcont_if_bot:
-  fixes bot and lub ("\<Or> _" [900] 900) and ord (infix "\<sqsubseteq>" 60)
+  fixes bot and lub ("\<Or>") and ord (infix "\<sqsubseteq>" 60)
   assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt"
   and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"
@@ -877,7 +877,7 @@
 end
 
 lemma admissible_leI:
-  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or> _" [900] 900)
+  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>")
   assumes "class.ccpo lub (\<sqsubseteq>) (mk_less (\<sqsubseteq>))"
   and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. f x)"
   and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. g x)"