Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / model / monoids / Qmonoid.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/monoids/Qmonoid.mma b/helm/software/matita/contribs/CoRN-Procedural/model/monoids/Qmonoid.mma
index bf45b45e2f4f12e5e0fe20bda013a2a0023bfae1..3acc779a60bb2f6b73361776789cf42eebc8cec6 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/monoids/Qmonoid.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/monoids/Qmonoid.mma
@@ -27,23 +27,23 @@ include "algebra/CMonoids.ma".
 The rational numbers form with addition a CMonoid. [QZERO] is the unit.
 *)
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_rht_unit3.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_rht_unit3.con" as lemma.
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_lft_unit3.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_lft_unit3.con" as lemma.
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_is_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_is_CMonoid.con" as definition.
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_as_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_as_CMonoid.con" as definition.
 
 (*#* ***$\langle$#⟨#[Q],[[*]]$\rangle$#⟩#
 Also with multiplication Q forms a CMonoid. Here, the unit is [QONE].
 *)
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_rht_unit.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_rht_unit.con" as lemma.
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_lft_unit.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_lft_unit.con" as lemma.
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_is_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_is_CMonoid.con" as definition.
 
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_as_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_as_CMonoid.con" as definition.