set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
*)
(* UNEXPORTED
-Section Sums.
+Section Sums
*)
-inline "cic:/CoRN/algebra/CSums/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSums/Sums/G.var".
(* Sum1 and Sum use subtraction *)
inline "cic:/CoRN/algebra/CSums/Sumx_Sum0.con".
(* UNEXPORTED
-End Sums.
+End Sums
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section More_Sums.
+Section More_Sums
*)
-inline "cic:/CoRN/algebra/CSums/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var".
inline "cic:/CoRN/algebra/CSums/Mengolli_Sum.con".
inline "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con".
(* UNEXPORTED
-End More_Sums.
+End More_Sums
*)
(* UNEXPORTED