X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Ftend.ma;h=a9372d26dee5f47b81809d3f25a8919b3129b329;hb=e1efca300fbaeb8c69a691a428a084d89a2c058f;hp=84d30a8fe39450aa071c6e9e92316583c5c5f132;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/tend.ma b/helm/software/matita/contribs/dama/dama_duality/tend.ma
index 84d30a8fe..a9372d26d 100644
--- a/helm/software/matita/contribs/dama/dama_duality/tend.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/tend.ma
@@ -23,5 +23,5 @@ 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}.
-interpretation "tends to" 'tends s x = (tends0 _ (d2s _ _ s x)).
+interpretation "tends to" 'tends s x = (tends0 ? (d2s ? ? s x)).