- notation fixed according to the new stricter semantics

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

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 8aacb5b59214bafbb89911b4ca3f9530823f06d8..326681b2608d2ce0c0bc673d41aa43d73cd8b04e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -96,7 +96,7 @@ lemma bs_of_ss:
  ∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝ 
   λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
 
-notation < "x \sub \neq" left associative with precedence 91 for @{'bsss $x}.
+notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
 interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
 alias symbol "square" (instance 7) = "ordered set square".
@@ -108,7 +108,7 @@ lemma ss_of_bs:
  λO:ordered_set.λu,v:O.
   λb:(O:bishop_set) square.λH1,H2.〈〈fst b,H1〉,〈snd b,H2〉〉.
 
-notation < "x \sub \nleq" left associative with precedence 91 for @{'ssbs $x}.
+notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}.
 interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).
 
 lemma segment_ordered_uniform_space: