X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fmodel%2Fmonoids%2FNmonoid.ma;h=4eac5c0c6ff3f865f13b13ff9a3d3eac03c2c833;hb=f104e234238586ac846881feb30e1b56a509cfd3;hp=80ea8fdc0169c19522bf69ab08b4d1788bbf9a6d;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma b/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma
index 80ea8fdc0..4eac5c0c6 100644
--- a/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma
+++ b/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma
@@ -16,29 +16,27 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Nmonoid".
 
+include "CoRN.ma".
+
 (* $Id: Nmonoid.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *)
 
-(* INCLUDE
-Nsemigroup
-*)
+include "model/semigroups/Nsemigroup.ma".
 
-(* INCLUDE
-CMonoids
-*)
+include "algebra/CMonoids.ma".
 
 (*#* **Example of a monoid: $\langle$#⟨#[nat],[[+]]$\rangle$#⟩#
 Zero is an unit for the addition.
 *)
 
-inline cic:/CoRN/model/monoids/Nmonoid/O_as_rht_unit.con.
+inline "cic:/CoRN/model/monoids/Nmonoid/O_as_rht_unit.con".
 
-inline cic:/CoRN/model/monoids/Nmonoid/O_as_lft_unit.con.
+inline "cic:/CoRN/model/monoids/Nmonoid/O_as_lft_unit.con".
 
-inline cic:/CoRN/model/monoids/Nmonoid/nat_is_CMonoid.con.
+inline "cic:/CoRN/model/monoids/Nmonoid/nat_is_CMonoid.con".
 
 (*#*
  Whence we can define #<i>#%\emph{%the monoid of natural numbers%}%#</i>#:
 *)
 
-inline cic:/CoRN/model/monoids/Nmonoid/nat_as_CMonoid.con.
+inline "cic:/CoRN/model/monoids/Nmonoid/nat_as_CMonoid.con".