X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSums.ma;h=b0fc1c6a256da0e1904891ecb350b9ea71a3a568;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=0177138c73ca71f48d8378048b4fa3e102f01ed3;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
index 0177138c7..b0fc1c6a2 100644
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums".
 
+include "CoRN.ma".
+
 (* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
 
 (*#* printing Sum0 %\ensuremath{\sum_0}% #&sum;<sub>0</sub># *)
@@ -28,13 +30,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums".
 
 (*#* printing Sumx %\ensuremath{\sum'}% #&sum;'&*)
 
-(* INCLUDE
-CAbGroups
-*)
-
-(* INCLUDE
-Peano_dec
-*)
+include "algebra/CAbGroups.ma".
 
 (*#* * Sums
 
@@ -46,13 +42,13 @@ Peano_dec
 Section Sums.
 *)
 
-inline cic:/CoRN/algebra/CSums/G.var.
+inline "cic:/CoRN/algebra/CSums/G.var".
 
 (* Sum1 and Sum use subtraction *)
 
-inline cic:/CoRN/algebra/CSums/Sumlist.con.
+inline "cic:/CoRN/algebra/CSums/Sumlist.con".
 
-inline cic:/CoRN/algebra/CSums/Sumx.con.
+inline "cic:/CoRN/algebra/CSums/Sumx.con".
 
 (*#*
 It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$
@@ -60,137 +56,137 @@ It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$
 [Zero] when the input is greater than or equal to [i].
 *)
 
-inline cic:/CoRN/algebra/CSums/part_tot_nat_fun.con.
+inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con".
 
-inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con.
+inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con".
 
-inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con.
+inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con".
 
 (*#* [Sum0] defines the sum for [i=0..(n-1)] *)
 
-inline cic:/CoRN/algebra/CSums/Sum0.con.
+inline "cic:/CoRN/algebra/CSums/Sum0.con".
 
 (*#* [Sum1] defines the sum for [i=m..(n-1)] *)
 
-inline cic:/CoRN/algebra/CSums/Sum1.con.
+inline "cic:/CoRN/algebra/CSums/Sum1.con".
 
-inline cic:/CoRN/algebra/CSums/Sum.con.
+inline "cic:/CoRN/algebra/CSums/Sum.con".
 
 (* Sum i=m..n *)
 
 (*#* [Sum2] is similar to [Sum1], but does not require the summand to be
 defined outside where it is being added. *)
 
-inline cic:/CoRN/algebra/CSums/Sum2.con.
+inline "cic:/CoRN/algebra/CSums/Sum2.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_one.con.
+inline "cic:/CoRN/algebra/CSums/Sum_one.con".
 
 (* UNEXPORTED
 Hint Resolve Sum_one: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sum_empty.con.
+inline "cic:/CoRN/algebra/CSums/Sum_empty.con".
 
 (* UNEXPORTED
 Hint Resolve Sum_empty: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sum_Sum.con.
+inline "cic:/CoRN/algebra/CSums/Sum_Sum.con".
 
 (* UNEXPORTED
 Hint Resolve Sum_Sum: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sum_first.con.
+inline "cic:/CoRN/algebra/CSums/Sum_first.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_last.con.
+inline "cic:/CoRN/algebra/CSums/Sum_last.con".
 
 (* UNEXPORTED
 Hint Resolve Sum_last: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sum_last'.con.
+inline "cic:/CoRN/algebra/CSums/Sum_last'.con".
 
 (*#*
 We add some extensionality results which will be quite useful
 when working with integration.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sum0_strext.con.
+inline "cic:/CoRN/algebra/CSums/Sum0_strext.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_strext.con.
+inline "cic:/CoRN/algebra/CSums/Sum_strext.con".
 
-inline cic:/CoRN/algebra/CSums/Sumx_strext.con.
+inline "cic:/CoRN/algebra/CSums/Sumx_strext.con".
 
-inline cic:/CoRN/algebra/CSums/Sum0_strext'.con.
+inline "cic:/CoRN/algebra/CSums/Sum0_strext'.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_strext'.con.
+inline "cic:/CoRN/algebra/CSums/Sum_strext'.con".
 
-inline cic:/CoRN/algebra/CSums/Sum0_wd.con.
+inline "cic:/CoRN/algebra/CSums/Sum0_wd.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_wd.con.
+inline "cic:/CoRN/algebra/CSums/Sum_wd.con".
 
-inline cic:/CoRN/algebra/CSums/Sumx_wd.con.
+inline "cic:/CoRN/algebra/CSums/Sumx_wd.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_wd'.con.
+inline "cic:/CoRN/algebra/CSums/Sum_wd'.con".
 
-inline cic:/CoRN/algebra/CSums/Sum2_wd.con.
+inline "cic:/CoRN/algebra/CSums/Sum2_wd.con".
 
-inline cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con.
+inline "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con".
 
 (* UNEXPORTED
 Hint Resolve Sum0_plus_Sum0: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sum_plus_Sum.con.
+inline "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con".
 
-inline cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con.
+inline "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con".
 
-inline cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con.
+inline "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con".
 
-inline cic:/CoRN/algebra/CSums/inv_Sum0.con.
+inline "cic:/CoRN/algebra/CSums/inv_Sum0.con".
 
 (* UNEXPORTED
 Hint Resolve inv_Sum0: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/inv_Sum.con.
+inline "cic:/CoRN/algebra/CSums/inv_Sum.con".
 
 (* UNEXPORTED
 Hint Resolve inv_Sum: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/inv_Sumx.con.
+inline "cic:/CoRN/algebra/CSums/inv_Sumx.con".
 
-inline cic:/CoRN/algebra/CSums/inv_Sum2.con.
+inline "cic:/CoRN/algebra/CSums/inv_Sum2.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_minus_Sum.con.
+inline "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con".
 
 (* UNEXPORTED
 Hint Resolve Sum_minus_Sum: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con.
+inline "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con".
 
-inline cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con.
+inline "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_apzero.con.
+inline "cic:/CoRN/algebra/CSums/Sum_apzero.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_zero.con.
+inline "cic:/CoRN/algebra/CSums/Sum_zero.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_term.con.
+inline "cic:/CoRN/algebra/CSums/Sum_term.con".
 
-inline cic:/CoRN/algebra/CSums/Sum0_shift.con.
+inline "cic:/CoRN/algebra/CSums/Sum0_shift.con".
 
 (* UNEXPORTED
 Hint Resolve Sum0_shift: algebra.
 *)
 
-inline cic:/CoRN/algebra/CSums/Sum_shift.con.
+inline "cic:/CoRN/algebra/CSums/Sum_shift.con".
 
-inline cic:/CoRN/algebra/CSums/Sum_big_shift.con.
+inline "cic:/CoRN/algebra/CSums/Sum_big_shift.con".
 
-inline cic:/CoRN/algebra/CSums/Sumx_Sum0.con.
+inline "cic:/CoRN/algebra/CSums/Sumx_Sum0.con".
 
 (* UNEXPORTED
 End Sums.
@@ -223,15 +219,15 @@ often referred to as ``Mengolli Sums''.
 Section More_Sums.
 *)
 
-inline cic:/CoRN/algebra/CSums/G.var.
+inline "cic:/CoRN/algebra/CSums/G.var".
 
-inline cic:/CoRN/algebra/CSums/Mengolli_Sum.con.
+inline "cic:/CoRN/algebra/CSums/Mengolli_Sum.con".
 
-inline cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con.
+inline "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con".
 
-inline cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con.
+inline "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con".
 
-inline cic:/CoRN/algebra/CSums/Sumx_to_Sum.con.
+inline "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con".
 
 (* UNEXPORTED
 End More_Sums.