X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2Foverlap%2Fo-algebra.ma;h=e4dcec62883084ac126cb5d513bbf4105a878e76;hb=5d669f492522b055f76c627eb89da97d0be05c2a;hp=40b2f72bb5dab9c2d53b979059e9b88bf0b7c063;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/nlibrary/overlap/o-algebra.ma b/matita/matita/nlibrary/overlap/o-algebra.ma
index 40b2f72bb..e4dcec628 100644
--- a/matita/matita/nlibrary/overlap/o-algebra.ma
+++ b/matita/matita/nlibrary/overlap/o-algebra.ma
@@ -70,11 +70,11 @@ for @{ 'overlap $a $b}.
 interpretation "o-algebra overlap" 'overlap a b = (fun11 ?? (fun11 ?? (oa_overlap ?) a) b).
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" 
-non associative with precedence 50 for @{ 'oa_meet $p }.
+non associative with precedence 55 for @{ 'oa_meet $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
 
-(*notation > "hovbox(∧ f)" non associative with precedence 60
+(*notation > "hovbox(∧ f)" non associative with precedence 65
 for @{ 'oa_meet $f }.
 interpretation "o-algebra meet" 'oa_meet f = 
   (fun12 ?? (oa_meet ??) f).
@@ -82,12 +82,12 @@ interpretation "o-algebra meet with explicit function" 'oa_meet_mk f =
   (fun12 ?? (oa_meet ??) (mk_unary_morphism ?? f ?)).
 *)
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" 
-non associative with precedence 50 for @{ 'oa_join $p }.
+non associative with precedence 55 for @{ 'oa_join $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
 
 (*CSC
-notation > "hovbox(∨ f)" non associative with precedence 60
+notation > "hovbox(∨ f)" non associative with precedence 65
 for @{ 'oa_join $f }.
 interpretation "o-algebra join" 'oa_join f = 
   (fun12 ?? (oa_join ??) f).
@@ -141,7 +141,7 @@ non associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
 notation < "hovbox(a ∨ b)" left associative with precedence 49
 for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 
-notation > "hovbox(∨ f)" non associative with precedence 59
+notation > "hovbox(∨ f)" non associative with precedence 64
 for @{ 'oa_join $f }.
 notation > "hovbox(a ∨ b)" left associative with precedence 49
 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.