set "baseuri" "cic:/matita/CoRN-Decl/reals/CauchySeq".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *)
Opaque IR.
*)
-inline "cic:/CoRN/reals/CauchySeq/IR.var".
+alias id "IR" = "cic:/CoRN/reals/CauchySeq/IR.var".
+
+(* NOTATION
+Notation PartIR := (PartFunct IR).
+*)
+
+(* NOTATION
+Notation ProjIR1 := (prj1 IR _ _ _).
+*)
+
+(* NOTATION
+Notation ProjIR2 := (prj2 IR _ _ _).
+*)
include "tactics/Transparent_algebra.ma".
(* begin hide *)
+(* NOTATION
+Notation ZeroR := (Zero:IR).
+*)
+
+(* NOTATION
+Notation OneR := (One:IR).
+*)
+
(* end hide *)
(* UNEXPORTED
-Section CReals_axioms.
+Section CReals_axioms
*)
(*#* ** [CReals] axioms *)
inline "cic:/CoRN/reals/CauchySeq/CauchySeqR.con".
(* UNEXPORTED
-End CReals_axioms.
+End CReals_axioms
*)
(* UNEXPORTED
-Section Cauchy_Defs.
+Section Cauchy_Defs
*)
(*#* ** Cauchy sequences
inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con".
(* UNEXPORTED
-End Cauchy_Defs.
+End Cauchy_Defs
*)
(* UNEXPORTED
-Section Inequalities.
+Section Inequalities
*)
(*#* *** Inequalities of Limits
inline "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con".
(* UNEXPORTED
-End Inequalities.
+End Inequalities
*)
(* UNEXPORTED
-Section Equiv_Cauchy.
+Section Equiv_Cauchy
*)
(*#* *** Equivalence of formulations of Cauchy *)
inline "cic:/CoRN/reals/CauchySeq/Lim_unique.con".
(* UNEXPORTED
-End Equiv_Cauchy.
+End Equiv_Cauchy
*)
(* UNEXPORTED
-Section Cauchy_props.
+Section Cauchy_props
*)
(*#* *** Properties of Cauchy sequences
inline "cic:/CoRN/reals/CauchySeq/Lim_mult.con".
(* UNEXPORTED
-End Cauchy_props.
+End Cauchy_props
*)