...

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/CPoly_Contin.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/CPoly_Contin.mma
index 6987ae2553efa551f484fabd03689b1fb436348c..a9e6c784ecb95e98730a374d71df883827ed1939 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/reals/CPoly_Contin.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/reals/CPoly_Contin.mma
@@ -22,11 +22,11 @@ include "CoRN.ma".
 
 include "reals/RealFuncts.ma".
 
-inline procedural "cic:/CoRN/reals/CPoly_Contin/plus_op_contin.con".
+inline procedural "cic:/CoRN/reals/CPoly_Contin/plus_op_contin.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CPoly_Contin/mult_op_contin.con".
+inline procedural "cic:/CoRN/reals/CPoly_Contin/mult_op_contin.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CPoly_Contin/linear_op_contin.con".
+inline procedural "cic:/CoRN/reals/CPoly_Contin/linear_op_contin.con" as lemma.
 
-inline procedural "cic:/CoRN/reals/CPoly_Contin/cpoly_op_contin.con".
+inline procedural "cic:/CoRN/reals/CPoly_Contin/cpoly_op_contin.con" as lemma.