X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FFunctSums.ma;h=aeed9200cd628be08d26e015b0ff7aac0b3226cd;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=5006a55f98b7ba36b8222f3768ea11b864043c31;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
index 5006a55f9..aeed9200c 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums".
 
+include "CoRN.ma".
+
 (* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *)
 
 (*#* printing FSum0 %\ensuremath{\sum_0}% #&sum;<sub>0</sub># *)
@@ -24,13 +26,9 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums".
 
 (*#* printing FSumx %\ensuremath{\sum'}% #&sum;'&*)
 
-(* INCLUDE
-CSumsReals
-*)
+include "reals/CSumsReals.ma".
 
-(* INCLUDE
-PartFunEquality
-*)
+include "ftc/PartFunEquality.ma".
 
 (*#* *Sums of Functions
 
@@ -48,9 +46,9 @@ $\sum_{i=m}^nf_i$#the sum of f<sub>m</sub> through f<sub>n</sub>#
 ( [FSum]).
 *)
 
-inline cic:/CoRN/ftc/FunctSums/FSum0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum.con".
 
 (*#*
 Although [FSum] is here defined directly, it has the same relationship
@@ -62,37 +60,37 @@ mentioned, their forming too big a type makes it impossible to use
 those results.
 *)
 
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum0_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_wd.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_one.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_one.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_first.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_first.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_last.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_last.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_last'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_last'.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_wd.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con".
 
-inline cic:/CoRN/ftc/FunctSums/inv_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/inv_FSum.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_wd'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_wd'.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_resp_less.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_resp_less.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con".
 
 (*#*
 Also important is the case when we have a finite family
@@ -100,15 +98,15 @@ $\{f_i\}_{i=0}^{n-1}$ of #exactly n# functions; in this case we need
 to use the [FSumx] operator.
 *)
 
-inline cic:/CoRN/ftc/FunctSums/FSumx.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx.con".
 
 (*#*
 This operator is well defined, as expected.
 *)
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_wd.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_wd'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_wd'.con".
 
 (*#*
 As was already the case for [Sumx], in many cases we will need to
@@ -117,9 +115,9 @@ explicitly assume that $f_i$#f<sub>1</sub># is independent of the proof that
 function $f_i$#f<sub>i</sub>#.
 *)
 
-inline cic:/CoRN/ftc/FunctSums/ext_fun_seq.con.
+inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq.con".
 
-inline cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con.
+inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con".
 
 (* UNEXPORTED
 Implicit Arguments ext_fun_seq [n].
@@ -133,35 +131,35 @@ Implicit Arguments ext_fun_seq' [n].
 Under these assumptions, we can characterize the domain and the value of the sum function from the domains and values of the summands:
 *)
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_pred.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_pred.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_pred'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_pred'.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_char.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_char.con".
 
 (*#*
 As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.
 *)
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_lt.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_lt.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSumx_le.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_le.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con".
 
 (*#*
 Some useful lemmas follow.
 *)
 
-inline cic:/CoRN/ftc/FunctSums/FSum0_0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_0.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum0_S.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_S.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_0.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_S.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_S.con".
 
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con".