- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / nlibrary / overlap / o-algebra.ma

diff --git a/matita/matita/nlibrary/overlap/o-algebra.ma b/matita/matita/nlibrary/overlap/o-algebra.ma
index 40b2f72bb5dab9c2d53b979059e9b88bf0b7c063..e4dcec62883084ac126cb5d513bbf4105a878e76 100644 (file)
--- 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)) }.