Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qabgroup.mma b/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qabgroup.mma
index 7dd20bc46b3c24ff313b7b996c22284a0f674025..568d785f4d3ce12a4bfdf36b092497e99c5836e9 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qabgroup.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qabgroup.mma
@@ -29,7 +29,7 @@ include "algebra/CAbGroups.ma".
 CAbGroup.
 *)
 
-inline procedural "cic:/CoRN/model/abgroups/Qabgroup/Q_is_CAbGroup.con".
+inline procedural "cic:/CoRN/model/abgroups/Qabgroup/Q_is_CAbGroup.con" as lemma.
 
-inline procedural "cic:/CoRN/model/abgroups/Qabgroup/Q_as_CAbGroup.con".
+inline procedural "cic:/CoRN/model/abgroups/Qabgroup/Q_as_CAbGroup.con" as definition.