]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
changelog to -rc-1
[helm.git] / matita / contribs / CoRN-Decl / algebra / CAbMonoids.ma
index 7f31fc1038725012a04cf2d6de792935df3abcc8..716750a783d564f29d07b17f77c216e1a0868057 100644 (file)
@@ -39,7 +39,7 @@ coercion cic:/matita/CoRN-Decl/algebra/CAbMonoids/cam_crr.con 0 (* compounds *).
 Section AbMonoid_Axioms
 *)
 
-inline "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/AbMonoid_Axioms/M.var" "Abelian_Monoids__AbMonoid_Axioms__".
+alias id "M" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/AbMonoid_Axioms/M.var".
 
 (*#*
 %\begin{convention}% Let [M] be an abelian monoid.
@@ -64,13 +64,13 @@ Section SubCAbMonoids
 ** Subgroups of an Abelian Monoid
 *)
 
-inline "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/M.var" "Abelian_Monoids__SubCAbMonoids__".
+alias id "M" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/M.var".
 
-inline "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/P.var" "Abelian_Monoids__SubCAbMonoids__".
+alias id "P" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/P.var".
 
-inline "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/Punit.var" "Abelian_Monoids__SubCAbMonoids__".
+alias id "Punit" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/Punit.var".
 
-inline "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/op_pres_P.var" "Abelian_Monoids__SubCAbMonoids__".
+alias id "op_pres_P" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/op_pres_P.var".
 
 (*#*
 %\begin{convention}%