Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / model / abgroups / QSposabgroup.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/QSposabgroup.mma b/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/QSposabgroup.mma
index ab852c45b94b069656ec7c809b8b3af4b144c3dd..e01f261c993b6b1b891d88943421c278071cf435 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/QSposabgroup.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/QSposabgroup.mma
@@ -26,7 +26,7 @@ include "algebra/CAbGroups.ma".
 The positive rational numbers form with the operation  $(x,y) \mapsto xy/2$  #(x,y) ↦ xy/2# an abelian group.
 *)
 
-inline procedural "cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_is_CAbGroup.con".
+inline procedural "cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_is_CAbGroup.con" as lemma.
 
-inline procedural "cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_as_CAbGroup.con".
+inline procedural "cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_as_CAbGroup.con" as definition.