X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCAbMonoids.ma;h=716750a783d564f29d07b17f77c216e1a0868057;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=7f31fc1038725012a04cf2d6de792935df3abcc8;hpb=62596f4e0a109e43c9df5da20571827c8b905ce4;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma b/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
index 7f31fc103..716750a78 100644
--- a/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
@@ -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}%