set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/Qposabgroup".
+include "CoRN_notation.ma".
+
(* $Id: Qposabgroup.v,v 1.6 2004/04/08 08:20:31 lcf Exp $ *)
-(* INCLUDE
-Qposgroup
-*)
+include "model/groups/Qposgroup.ma".
-(* INCLUDE
-CAbGroups
-*)
+include "algebra/CAbGroups.ma".
(*#* **Example of an abelian group: $\langle$#⟨#[Qpos],[[*]]$\rangle$#⟩#
The positive rationals form with the multiplication a CAbgroup.
*)
-inline cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_is_CAbGroup.con.
+inline "cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_is_CAbGroup.con".
-inline cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_as_CAbGroup.con.
+inline "cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_as_CAbGroup.con".