Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / reals / CSumsReals.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/CSumsReals.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/CSumsReals.mma
index ba22c080f9eb2167a3f2fc6b51e9b1ecd8b643e8..32313cff804457a63d571931f89a727351d7508f 100644 (file)
--- 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.