Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / model / structures / Qpossec.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qpossec.mma b/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qpossec.mma
index 946c0b922cb5c8cf41477061ae64bfb857ddf8c5..81d7c1c41aa042c802ff6e77117c42681d1c0f07 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qpossec.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qpossec.mma
@@ -31,28 +31,28 @@ We will prove some lemmas concerning rationals bigger than 0.
 One, two and four are all bigger than zero.
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/pos_QONE.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/pos_QONE.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/pos_QTWO.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/pos_QTWO.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/pos_QFOUR.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/pos_QFOUR.con" as lemma.
 
 (*#* A positive rational is not zero.
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/pos_imp_nonzero.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/pos_imp_nonzero.con" as definition.
 
 (*#* ***Multiplication
 The product of two positive rationals is again positive.
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/Qmult_pres_pos0.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/Qmult_pres_pos0.con" as lemma.
 
 (*#* ***Inverse
 The inverse of a positive rational is again positive.
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/inv_pres_pos0.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/inv_pres_pos0.con" as lemma.
 
 (*#* ***Special multiplication
 Now we will investigate the function $(x,y) \mapsto xy/2$#(x,y)
@@ -60,9 +60,9 @@ Now we will investigate the function $(x,y) \mapsto xy/2$#(x,y)
 \mapsto 4/x$ #x ↦ 4/x#.
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/QTWOpos_is_rht_unit0.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/QTWOpos_is_rht_unit0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/QTWOpos_is_left_unit0.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/QTWOpos_is_left_unit0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qpossec/multdiv2_is_inv.con".
+inline procedural "cic:/CoRN/model/structures/Qpossec/multdiv2_is_inv.con" as lemma.