ordered_set simplified

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

diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index 39c40194bca3c8db2133e149a8aa2a206fb8b979..948d14f67963ef2e929bba924e40edbe58572ea4 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -22,16 +22,16 @@ definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝
 
 coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
 
-notation < "hvbox((\lfloor p \rfloor) \sub ident i)" with precedence 70
+notation < "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
 for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
 
-notation > "hvbox((\lfloor p \rfloor) \sub ident i)" with precedence 70
+notation > "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
 for @{ 'sequence (\lambda ${ident i} . $p)}.
 
-notation > "hvbox(\lfloor ident i, p \rfloor)" with precedence 70
+notation > "hvbox(\lfloor ident i, term 19 p \rfloor)" with precedence 90
 for @{ 'sequence (\lambda ${ident i} . $p)}.
   
-notation "a \sub i" left associative with precedence 70 
+notation "a \sub i" left associative with precedence 90 
   for @{ 'sequence_appl $a $i }.
 
 interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).