set "baseuri" "cic:/matita/CoRN-Decl/reals/CSumsReals".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CSumsReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
*)
(* UNEXPORTED
-Section Sums_over_Reals.
+Section Sums_over_Reals
*)
-inline "cic:/CoRN/reals/CSumsReals/c.var".
+alias id "c" = "cic:/CoRN/reals/CSumsReals/Sums_over_Reals/c.var".
inline "cic:/CoRN/reals/CSumsReals/Sum0_c_exp.con".
*)
(* UNEXPORTED
-End Sums_over_Reals.
+End Sums_over_Reals
*)
(* UNEXPORTED