src/HOL/Complete_Lattices.thy
changeset 52141 eff000cab70f
parent 51540 eea5c4ca4a0e
child 52729 412c9e0381a1
--- a/src/HOL/Complete_Lattices.thy	Sat May 25 15:44:08 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sat May 25 15:44:29 2013 +0200
@@ -751,7 +751,7 @@
   "Inter S \<equiv> \<Sqinter>S"
   
 notation (xsymbols)
-  Inter  ("\<Inter>_" [90] 90)
+  Inter  ("\<Inter>_" [900] 900)
 
 lemma Inter_eq:
   "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
@@ -934,7 +934,7 @@
   "Union S \<equiv> \<Squnion>S"
 
 notation (xsymbols)
-  Union  ("\<Union>_" [90] 90)
+  Union  ("\<Union>_" [900] 900)
 
 lemma Union_eq:
   "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"