bla bla bla

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

diff --git a/helm/software/matita/contribs/dama/dama_duality/limit.ma b/helm/software/matita/contribs/dama/dama_duality/limit.ma
index 1250511e83ddda1573c8df1feca7b1d58878f74e..0b1bd1d3b8325fceb2074ef83c2bfc19a9e26327 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/limit.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/limit.ma
@@ -27,8 +27,8 @@ notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for
 notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}.
 notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}.
 
-interpretation "Excess limsup" 'limsup e s x = (cic:/matita/limit/limsup.con e s x).
-interpretation "Excess liminf" 'liminf e s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess limsup" 'limsup e s x = (limsup e s x).
+interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x).
 
 (* 3.29 *)  
 definition lim ≝ 
@@ -36,7 +36,7 @@ definition lim ≝
 
 notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}.
 notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}.
-interpretation "Excess lim" 'lim e s x = (cic:/matita/limit/lim.con e s x).
+interpretation "Excess lim" 'lim e s x = (lim e s x).
 
 lemma sup_decreasing:
   ∀E:excess.∀xn:sequence E.