set "baseuri" "cic:/matita/CoRN-Decl/algebra/Cauchy_COF".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
*)
(* UNEXPORTED
-Section Structure.
+Section Structure
*)
-inline "cic:/CoRN/algebra/Cauchy_COF/F.var".
+alias id "F" = "cic:/CoRN/algebra/Cauchy_COF/Structure/F.var".
(*#*
** Setoid Structure
inline "cic:/CoRN/algebra/Cauchy_COF/R_Set.con".
(* UNEXPORTED
-Section CSetoid_Structure.
+Section CSetoid_Structure
*)
inline "cic:/CoRN/algebra/Cauchy_COF/R_lt.con".
inline "cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con".
(* UNEXPORTED
-End CSetoid_Structure.
+End CSetoid_Structure
*)
(* UNEXPORTED
-Section Group_Structure.
+Section Group_Structure
*)
(*#*
inline "cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con".
(* UNEXPORTED
-End Group_Structure.
+End Group_Structure
*)
(* UNEXPORTED
-Section Ring_Structure.
+Section Ring_Structure
*)
(*#* ** Ring Structure
inline "cic:/CoRN/algebra/Cauchy_COF/R_CRing.con".
(* UNEXPORTED
-End Ring_Structure.
+End Ring_Structure
*)
(* UNEXPORTED
-Section Field_Structure.
+Section Field_Structure
*)
(*#* ** Field Structure
inline "cic:/CoRN/algebra/Cauchy_COF/R_CField.con".
(* UNEXPORTED
-End Field_Structure.
+End Field_Structure
*)
(* UNEXPORTED
-Section Order.
+Section Order
*)
(*#* ** Order Structure
inline "cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con".
(* UNEXPORTED
-End Order.
+End Order
*)
(*#*
*)
(* UNEXPORTED
-Section Auxiliary.
+Section Auxiliary
*)
inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con".
inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con".
(* UNEXPORTED
-End Auxiliary.
+End Auxiliary
*)
(* UNEXPORTED
-End Structure.
+End Structure
*)