- setters for data structures now support "commuting conversion"-like

[helm.git] / helm / software / matita / contribs / CoRN-Decl / reals / CauchySeq.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma b/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
index a8ab031a01d3f31f762abdcdbe002b4afdf0eaf2..4bc6c7aa18e1185dc7bf81a0ffc891253c5e5c09 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
@@ -16,7 +16,7 @@
 
 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 $ *)
 
@@ -43,16 +43,36 @@ Definition IR : CReals := Concrete_R.
 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 *)
@@ -74,11 +94,11 @@ inline "cic:/CoRN/reals/CauchySeq/str_Archimedes.con".
 inline "cic:/CoRN/reals/CauchySeq/CauchySeqR.con".
 
 (* UNEXPORTED
-End CReals_axioms.
+End CReals_axioms
 *)
 
 (* UNEXPORTED
-Section Cauchy_Defs.
+Section Cauchy_Defs
 *)
 
 (*#* ** Cauchy sequences
@@ -149,11 +169,11 @@ inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con".
 inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con".
 
 (* UNEXPORTED
-End Cauchy_Defs.
+End Cauchy_Defs
 *)
 
 (* UNEXPORTED
-Section Inequalities.
+Section Inequalities
 *)
 
 (*#* *** Inequalities of Limits
@@ -195,11 +215,11 @@ inline "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con".
 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 *)
@@ -247,11 +267,11 @@ inline "cic:/CoRN/reals/CauchySeq/Lim_wd'.con".
 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
@@ -290,6 +310,6 @@ inline "cic:/CoRN/reals/CauchySeq/Cauchy_mult.con".
 inline "cic:/CoRN/reals/CauchySeq/Lim_mult.con".
 
 (* UNEXPORTED
-End Cauchy_props.
+End Cauchy_props
 *)