X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Finfsup.ma;h=b5ff03f0a8d653be9899a35f56e20ce08c7c7dc0;hb=99f153e43f18bc682339bed41c8230af2ac6fd2f;hp=cc3292fd0b5178775d5199ba3bc5d850570a6e38;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/infsup.ma b/helm/software/matita/contribs/dama/dama_duality/infsup.ma
index cc3292fd0..b5ff03f0a 100644
--- a/helm/software/matita/contribs/dama/dama_duality/infsup.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/infsup.ma
@@ -39,12 +39,12 @@ notation > "s 'is_decreasing' 'in' e"    non associative with precedence 50 for
 notation > "x 'is_strong_sup' s 'in' e"  non associative with precedence 50 for @{'strong_sup $e $s $x}.
 notation > "x 'is_strong_inf' s 'in' e"  non associative with precedence 50 for @{'strong_inf $e $s $x}.
 
-interpretation "Excess upper bound" 'upper_bound e s x = (cic:/matita/infsup/upper_bound.con e s x).
-interpretation "Excess lower bound" 'lower_bound e s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con e) s x).
-interpretation "Excess increasing"  'increasing e s    = (cic:/matita/infsup/increasing.con e s).
-interpretation "Excess decreasing"  'decreasing e s    = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con e) s).
-interpretation "Excess strong sup"  'strong_sup e s x  = (cic:/matita/infsup/strong_sup.con e s x).
-interpretation "Excess strong inf"  'strong_inf e s x  = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess upper bound" 'upper_bound e s x = (upper_bound e s x).
+interpretation "Excess lower bound" 'lower_bound e s x = (upper_bound (dual_exc e) s x).
+interpretation "Excess increasing"  'increasing e s    = (increasing e s).
+interpretation "Excess decreasing"  'decreasing e s    = (increasing (dual_exc e) s).
+interpretation "Excess strong sup"  'strong_sup e s x  = (strong_sup e s x).
+interpretation "Excess strong inf"  'strong_inf e s x  = (strong_sup (dual_exc e) s x).
 
 lemma strong_sup_is_weak: 
   ∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.