X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fsubsets.ma;fp=matita%2Fmatita%2Flib%2Fformal_topology%2Fsubsets.ma;h=8bacd2a5538ce15df4168e0e9675a69d69dd69c0;hb=eaaea3c18083de3e442e939768ff450d3b093911;hp=15bfb98d3b395b78e4c80c78514a0b63de252e2a;hpb=dc66c8d89a5147178ccdacb8341ed26c9c52f06b;p=helm.git

diff --git a/matita/matita/lib/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma
index 15bfb98d3..8bacd2a55 100644
--- a/matita/matita/lib/formal_topology/subsets.ma
+++ b/matita/matita/lib/formal_topology/subsets.ma
@@ -164,16 +164,16 @@ definition big_union: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
 qed.
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (\emsp) term 90 p)" 
-non associative with precedence 50 for @{ 'bigcup $p }.
+non associative with precedence 55 for @{ 'bigcup $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
-notation > "hovbox(⋃ f)" non associative with precedence 60 for @{ 'bigcup $f }.
+non associative with precedence 55 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋃ f)" non associative with precedence 65 for @{ 'bigcup $f }.
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (\emsp) term 90 p)" 
-non associative with precedence 50 for @{ 'bigcap $p }.
+non associative with precedence 55 for @{ 'bigcap $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }.
-notation > "hovbox(⋂ f)" non associative with precedence 60 for @{ 'bigcap $f }.
+non associative with precedence 55 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋂ f)" non associative with precedence 65 for @{ 'bigcap $f }.
 
 interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f).
 interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f).