set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *)
inline "cic:/CoRN/algebra/CGroups/CGroup.ind".
-coercion "cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con 0 (* compounds *).
(* End_SpecReals *)
Implicit Arguments cg_inv [c].
*)
+(* NOTATION
+Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
+*)
+
inline "cic:/CoRN/algebra/CGroups/cg_minus.con".
(*#*
Implicit Arguments cg_minus [G].
*)
+(* NOTATION
+Infix "[-]" := cg_minus (at level 50, left associativity).
+*)
+
(* End_SpecReals *)
(*#*
*)
(* UNEXPORTED
-Section CGroup_axioms.
+Section CGroup_axioms
*)
-inline "cic:/CoRN/algebra/CGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_axioms/G.var".
inline "cic:/CoRN/algebra/CGroups/cg_inverse.con".
(* UNEXPORTED
-End CGroup_axioms.
+End CGroup_axioms
*)
(*#*
*)
(* UNEXPORTED
-Section CGroup_basics.
+Section CGroup_basics
*)
-inline "cic:/CoRN/algebra/CGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_basics/G.var".
inline "cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con".
*)
(* UNEXPORTED
-Section SubCGroups.
+Section SubCGroups
*)
-inline "cic:/CoRN/algebra/CGroups/P.var".
+alias id "P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/P.var".
-inline "cic:/CoRN/algebra/CGroups/Punit.var".
+alias id "Punit" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/Punit.var".
-inline "cic:/CoRN/algebra/CGroups/op_pres_P.var".
+alias id "op_pres_P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/op_pres_P.var".
-inline "cic:/CoRN/algebra/CGroups/inv_pres_P.var".
+alias id "inv_pres_P" = "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/inv_pres_P.var".
-inline "cic:/CoRN/algebra/CGroups/subcrr.con".
+inline "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subcrr.con" "CGroup_basics__SubCGroups__".
-inline "cic:/CoRN/algebra/CGroups/subinv.con".
+inline "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subinv.con" "CGroup_basics__SubCGroups__".
inline "cic:/CoRN/algebra/CGroups/isgrp_scrr.con".
inline "cic:/CoRN/algebra/CGroups/Build_SubCGroup.con".
(* UNEXPORTED
-End SubCGroups.
+End SubCGroups
*)
(* UNEXPORTED
-End CGroup_basics.
+End CGroup_basics
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Assoc_properties.
+Section Assoc_properties
*)
-inline "cic:/CoRN/algebra/CGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CGroups/Assoc_properties/G.var".
inline "cic:/CoRN/algebra/CGroups/assoc_2.con".
inline "cic:/CoRN/algebra/CGroups/plus_resp_eq.con".
(* UNEXPORTED
-End Assoc_properties.
+End Assoc_properties
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section cgroups_apartness.
+Section cgroups_apartness
*)
-inline "cic:/CoRN/algebra/CGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CGroups/cgroups_apartness/G.var".
inline "cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con".
inline "cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con".
(* UNEXPORTED
-End cgroups_apartness.
+End cgroups_apartness
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section CGroup_Ops.
+Section CGroup_Ops
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/G.var".
-inline "cic:/CoRN/algebra/CGroups/F.var".
+alias id "F" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/F.var".
-inline "cic:/CoRN/algebra/CGroups/F'.var".
+alias id "F'" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/F'.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CGroups/P.con".
+inline "cic:/CoRN/algebra/CGroups/CGroup_Ops/P.con" "CGroup_Ops__".
-inline "cic:/CoRN/algebra/CGroups/Q.con".
+inline "cic:/CoRN/algebra/CGroups/CGroup_Ops/Q.con" "CGroup_Ops__".
(* end hide *)
(* UNEXPORTED
-Section Part_Function_Inv.
+Section Part_Function_Inv
*)
inline "cic:/CoRN/algebra/CGroups/part_function_inv_strext.con".
inline "cic:/CoRN/algebra/CGroups/Finv.con".
(* UNEXPORTED
-End Part_Function_Inv.
+End Part_Function_Inv
*)
(* UNEXPORTED
-Section Part_Function_Minus.
+Section Part_Function_Minus
*)
inline "cic:/CoRN/algebra/CGroups/part_function_minus_strext.con".
inline "cic:/CoRN/algebra/CGroups/Fminus.con".
(* UNEXPORTED
-End Part_Function_Minus.
+End Part_Function_Minus
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CGroups/R.var".
+alias id "R" = "cic:/CoRN/algebra/CGroups/CGroup_Ops/R.var".
inline "cic:/CoRN/algebra/CGroups/included_FInv.con".
inline "cic:/CoRN/algebra/CGroups/included_FMinus''.con".
(* UNEXPORTED
-End CGroup_Ops.
+End CGroup_Ops
*)
(* UNEXPORTED
Implicit Arguments Finv [G].
*)
+(* NOTATION
+Notation "{--} x" := (Finv x) (at level 2, right associativity).
+*)
+
(* UNEXPORTED
Implicit Arguments Fminus [G].
*)
+(* NOTATION
+Infix "{-}" := Fminus (at level 50, left associativity).
+*)
+
(* UNEXPORTED
Hint Resolve included_FInv included_FMinus : included.
*)