Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / model / rings / Qring.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/rings/Qring.mma b/helm/software/matita/contribs/CoRN-Procedural/model/rings/Qring.mma
index 91bf33b9cbc3ffe440f42dc914687e76a2644c07..a35056ca35f752dbe0ec8ead0a4f8b376491fbe0 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/rings/Qring.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/rings/Qring.mma
@@ -29,18 +29,18 @@ Because [Q] forms an abelian group with addition, a monoid with
 multiplication and it satisfies the distributive law, it is a ring.
 *)
 
-inline procedural "cic:/CoRN/model/rings/Qring/Q_mult_plus_is_dist.con".
+inline procedural "cic:/CoRN/model/rings/Qring/Q_mult_plus_is_dist.con" as lemma.
 
-inline procedural "cic:/CoRN/model/rings/Qring/Q_is_CRing.con".
+inline procedural "cic:/CoRN/model/rings/Qring/Q_is_CRing.con" as definition.
 
-inline procedural "cic:/CoRN/model/rings/Qring/Q_as_CRing.con".
+inline procedural "cic:/CoRN/model/rings/Qring/Q_as_CRing.con" as definition.
 
 (*#* The following lemmas are used in the proof that [Q] is Archimeadian.
 *)
 
-inline procedural "cic:/CoRN/model/rings/Qring/injz_Nring.con".
+inline procedural "cic:/CoRN/model/rings/Qring/injz_Nring.con" as lemma.
 
-inline procedural "cic:/CoRN/model/rings/Qring/injZ_eq.con".
+inline procedural "cic:/CoRN/model/rings/Qring/injZ_eq.con" as lemma.
 
-inline procedural "cic:/CoRN/model/rings/Qring/nring_Q.con".
+inline procedural "cic:/CoRN/model/rings/Qring/nring_Q.con" as lemma.