few more steps

[helm.git] / helm / software / matita / contribs / dama / dama_duality / tend.ma

diff --git a/helm/software/matita/contribs/dama/dama_duality/tend.ma b/helm/software/matita/contribs/dama/dama_duality/tend.ma
index a5bf7501acf7047c91527b552f1cac1c6d82922d..84d30a8fe39450aa071c6e9e92316583c5c5f132 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/tend.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/tend.ma
@@ -23,6 +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 = 
-  (cic:/matita/tend/tends0.con _ (cic:/matita/tend/d2s.con _ _ s x)).
+interpretation "tends to" 'tends s x = (tends0 _ (d2s _ _ s x)).