diff -r 88a69da5d3fa -r eff000cab70f src/HOL/Complete_Lattices.thy --- 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 \ \S" notation (xsymbols) - Inter ("\_" [90] 90) + Inter ("\_" [900] 900) lemma Inter_eq: "\A = {x. \B \ A. x \ B}" @@ -934,7 +934,7 @@ "Union S \ \S" notation (xsymbols) - Union ("\_" [90] 90) + Union ("\_" [900] 900) lemma Union_eq: "\A = {x. \B \ A. x \ B}"