X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Freals%2FCSumsReals.mma;h=32313cff804457a63d571931f89a727351d7508f;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=ba22c080f9eb2167a3f2fc6b51e9b1ecd8b643e8;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/CSumsReals.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/CSumsReals.mma
index ba22c080f..32313cff8 100644
--- a/helm/software/matita/contribs/CoRN-Procedural/reals/CSumsReals.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/reals/CSumsReals.mma
@@ -36,13 +36,13 @@ Section Sums_over_Reals
 
 alias id "c" = "cic:/CoRN/reals/CSumsReals/Sums_over_Reals/c.var".
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_c_exp.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_c_exp.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sum0_c_exp.
 *)
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum_c_exp.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum_c_exp.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sum_c_exp.
@@ -50,7 +50,7 @@ Hint Resolve Sum_c_exp.
 
 (*#* The following formulation is often more useful if [c [<] 1]. *)
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum_c_exp'.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum_c_exp'.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sum_c_exp'.
@@ -64,29 +64,29 @@ End Sums_over_Reals
 Hint Resolve Sum0_c_exp Sum_c_exp Sum_c_exp': algebra.
 *)
 
-inline procedural "cic:/CoRN/reals/CSumsReals/diff_is_Sum0.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/diff_is_Sum0.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/diff_is_sum.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/diff_is_sum.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_pres_less.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_pres_less.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum_pres_less.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum_pres_less.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum_pres_leEq.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum_pres_leEq.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_comm_scal.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_comm_scal.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sum0_comm_scal: algebra.
 *)
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum_comm_scal.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum_comm_scal.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_comm_scal'.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_comm_scal'.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum_comm_scal'.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum_comm_scal'.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sumx_comm_scal'.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sumx_comm_scal'.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CSumsReals/Sum2_comm_scal'.con".
+inline procedural "cic:/CoRN/reals/CSumsReals/Sum2_comm_scal'.con" as lemma.