- notation fixed according to the new stricter semantics

[helm.git] / helm / software / matita / contribs / dama / dama / uniform.ma

diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index faba6d83a68be9cc9f2e45d04b4a661072961b2b..ed9e6fe5d1d60a66ddf205d8e1bbcbe7f0ffd113 100644 (file)
--- 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).