include "algebra/CMonoids.ma".
(* UNEXPORTED
-Section Abelian_Monoids.
+Section Abelian_Monoids
*)
(*#*
inline "cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind".
-coercion "cic:/matita/CoRN-Decl/algebra/CAbMonoids/cam_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CAbMonoids/cam_crr.con 0 (* compounds *).
(* UNEXPORTED
-Section AbMonoid_Axioms.
+Section AbMonoid_Axioms
*)
-inline "cic:/CoRN/algebra/CAbMonoids/M.var".
+alias id "M" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/AbMonoid_Axioms/M.var".
(*#*
%\begin{convention}% Let [M] be an abelian monoid.
inline "cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con".
(* UNEXPORTED
-End AbMonoid_Axioms.
+End AbMonoid_Axioms
*)
(* UNEXPORTED
-Section SubCAbMonoids.
+Section SubCAbMonoids
*)
(*#*
** Subgroups of an Abelian Monoid
*)
-inline "cic:/CoRN/algebra/CAbMonoids/M.var".
+alias id "M" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/M.var".
-inline "cic:/CoRN/algebra/CAbMonoids/P.var".
+alias id "P" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/P.var".
-inline "cic:/CoRN/algebra/CAbMonoids/Punit.var".
+alias id "Punit" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/Punit.var".
-inline "cic:/CoRN/algebra/CAbMonoids/op_pres_P.var".
+alias id "op_pres_P" = "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/op_pres_P.var".
(*#*
%\begin{convention}%
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CAbMonoids/subcrr.con".
+inline "cic:/CoRN/algebra/CAbMonoids/Abelian_Monoids/SubCAbMonoids/subcrr.con" "Abelian_Monoids__SubCAbMonoids__".
inline "cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con".
inline "cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con".
(* UNEXPORTED
-End SubCAbMonoids.
+End SubCAbMonoids
*)
(* UNEXPORTED
-End Abelian_Monoids.
+End Abelian_Monoids
*)
(* UNEXPORTED