X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Flimit.ma;h=0b1bd1d3b8325fceb2074ef83c2bfc19a9e26327;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=1250511e83ddda1573c8df1feca7b1d58878f74e;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/limit.ma b/helm/software/matita/contribs/dama/dama_duality/limit.ma
index 1250511e8..0b1bd1d3b 100644
--- 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.