X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Ftend.ma;h=1d14b49abf19f8848185b86c957f1cab638810c5;hb=5f1066ffb3c6ed53f9bf17ae2a81a9c9db32dba7;hp=a9372d26dee5f47b81809d3f25a8919b3129b329;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/contribs/dama/dama_duality/tend.ma b/matita/matita/contribs/dama/dama_duality/tend.ma
index a9372d26d..1d14b49ab 100644
--- a/matita/matita/contribs/dama/dama_duality/tend.ma
+++ b/matita/matita/contribs/dama/dama_duality/tend.ma
@@ -22,6 +22,6 @@ definition tends0 ≝
 definition d2s ≝ 
   λR.λms:metric_space R.λs:sequence ms.λk.λn. δ (s n) k.
 
-notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
+notation "s ⇝ x" non associative with precedence 55 for @{'tends $s $x}.
 interpretation "tends to" 'tends s x = (tends0 ? (d2s ? ? s x)).