X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2FlambdaN%2Flambda_notation.ma;h=57c02e03ac11a937f855ce181eee4484d97ca42d;hb=3fc94a73952678239bed11c605e180163f924c10;hp=596424938e459fb0e62d51f5e8fd0bc5d13b475b;hpb=15190ed1fb47989f2d50261db7991186ec3d5e47;p=helm.git

diff --git a/matita/matita/lib/lambdaN/lambda_notation.ma b/matita/matita/lib/lambdaN/lambda_notation.ma
index 596424938..57c02e03a 100644
--- a/matita/matita/lib/lambdaN/lambda_notation.ma
+++ b/matita/matita/lib/lambdaN/lambda_notation.ma
@@ -23,18 +23,18 @@ notation "hvbox(a break (≅ ^ term 90 c) b)"
   non associative with precedence 45
   for @{'Eq1 $c $a $b}.
 
-notation "hbox(! term 50 a)"
-  non associative with precedence 50
+notation "hbox(! term 55 a)"
+  non associative with precedence 55
   for @{'Invariant $a}.
 
-notation "hbox((! ^ term 90 b) term 50 a)"
-  non associative with precedence 50
+notation "hbox((! ^ term 90 b) term 55 a)"
+  non associative with precedence 55
   for @{'Invariant1 $a $b}.
 
 (* lifting, substitution *)
 
 notation "hvbox(↑ [ p break , k ] break t)"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'Lift1 $p $k $t}.
 
 notation "hvbox(M break [ / l ])"
@@ -58,37 +58,37 @@ notation "hvbox(G break  ⊢ A break ÷ B)"
 (* interpretations *)
 
 notation "hvbox(║T║)"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'IInt $T}.
 
 notation "hvbox(║T║ break _ [E])"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'IInt1 $T $E}.
 
 notation "hvbox(║T║ break _ [E1 break , E2])"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'IInt2 $T $E1 $E2}.
 
 notation "hvbox(〚T〛)"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'EInt $T}.
 
 notation "hvbox(〚T〛 break _ [E])"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'EInt1 $T $E}.
 
 notation "hvbox(〚T〛 break _ [E1 break , E2])"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'EInt2 $T $E1 $E2}.
 
 notation "hvbox(《T》)"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'XInt $T}.
 
 notation "hvbox(《T》 break _ [E])"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'XInt1 $T $E}.
 
 notation "hvbox(《T》 break _ [E1 break , E2])"
-   non associative with precedence 50
+   non associative with precedence 55
    for @{'XInt2 $T $E1 $E2}.