X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Funiform.ma;h=ed9e6fe5d1d60a66ddf205d8e1bbcbe7f0ffd113;hb=25aa80d913c903fcc270d05464cf3084b12d52a8;hp=faba6d83a68be9cc9f2e45d04b4a661072961b2b;hpb=cb2419357a3f80388f71eb2730bff154bd4ef000;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index faba6d83a..ed9e6fe5d 100644
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -35,12 +35,10 @@ definition invert_bs_relation ≝
   λC:bishop_set.λU:C square → Prop.
     λx:C square. U 〈snd x,fst x〉.
     
-notation < "s \sup (-1)"  left associative with precedence 70
-  for @{ 'invert $s }.
-notation < "s \sup (-1) x"  left associative with precedence 70
+notation < "s \sup (-1)"  with precedence 70 for @{ 'invert $s }.
+notation < "s \sup (-1) x"  with precedence 70
   for @{ 'invert_appl $s $x}. 
-notation > "'inv'" right associative with precedence 70
-  for @{ 'invert_symbol  }.
+notation > "'inv'" with precedence 70 for @{ 'invert_symbol  }.
 interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
 interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
 interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).