Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/monoids/QSposmonoid.mma b/helm/software/matita/contribs/CoRN-Procedural/model/monoids/QSposmonoid.mma
index 6dfd8114bec79b9da55909f15205d67bee689cd4..50866dfdf6534c52df3715b04080c6b07f7a8a10 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/monoids/QSposmonoid.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/monoids/QSposmonoid.mma
@@ -27,11 +27,11 @@ Two is the unit of the operation  $(x,y) \mapsto xy/2$ #(x,y)
   ↦ xy/2# on the positive rationals. So we have another monoid structure on the positive rational numbers.
 *)
 
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_rht_unit.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_rht_unit.con" as lemma.
 
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_lft_unit.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_lft_unit.con" as lemma.
 
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_is_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_is_CMonoid.con" as definition.
 
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_as_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_as_CMonoid.con" as definition.