...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / algebra / CAbMonoids.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/algebra/CAbMonoids.mma b/helm/software/matita/contribs/CoRN-Procedural/algebra/CAbMonoids.mma
index b639df6cc71daf203139dd870aa1c6f4acde8193..b1bce83624d2f62e158148f9c909fe962344d0f8 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/algebra/CAbMonoids.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/algebra/CAbMonoids.mma
@@ -27,7 +27,7 @@ Section Abelian_Monoids
 Now we introduce commutativity and add some results.
 *)
 
-inline procedural "cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con".
+inline procedural "cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con" as definition.
 
 inline procedural "cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind".
 
@@ -39,18 +39,20 @@ cic:/matita/CoRN-Procedural/algebra/CAbMonoids/cam_crr.con
 Section AbMonoid_Axioms
 *)
 
-alias id "M" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/AbMonoid_Axioms/M.var".
+(* UNEXPORTED
+cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/AbMonoid_Axioms/M.var
+*)
 
 (*#*
 %\begin{convention}% Let [M] be an abelian monoid.
 %\end{convention}%
 *)
 
-inline procedural "cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con".
+inline procedural "cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CAbMonoids/cam_commutes.con".
+inline procedural "cic:/CoRN/algebra/CAbMonoids/cam_commutes.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con".
+inline procedural "cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con" as lemma.
 
 (* UNEXPORTED
 End AbMonoid_Axioms
@@ -64,13 +66,21 @@ Section SubCAbMonoids
 ** Subgroups of an Abelian Monoid
 *)
 
-alias id "M" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/M.var".
+(* UNEXPORTED
+cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/M.var
+*)
 
-alias id "P" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/P.var".
+(* UNEXPORTED
+cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/P.var
+*)
 
-alias id "Punit" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/Punit.var".
+(* UNEXPORTED
+cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/Punit.var
+*)
 
-alias id "op_pres_P" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/op_pres_P.var".
+(* UNEXPORTED
+cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/op_pres_P.var
+*)
 
 (*#*
 %\begin{convention}%
@@ -79,11 +89,11 @@ that contains [Zero] and is closed under [[+]] and [[--]].
 %\end{convention}%
 *)
 
-inline procedural "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/subcrr.con" "Abelian_Monoids__SubCAbMonoids__".
+inline procedural "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/subcrr.con" "Abelian_Monoids__SubCAbMonoids__" as definition.
 
-inline procedural "cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con".
+inline procedural "cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con".
+inline procedural "cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con" as definition.
 
 (* UNEXPORTED
 End SubCAbMonoids