X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Freals%2FCauchySeq.ma;h=4bc6c7aa18e1185dc7bf81a0ffc891253c5e5c09;hb=378a122bd40f832581ee3e82cc428584b6579a57;hp=e019be0736b37e6f5dc5bb32bd84a3df3d388f22;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/reals/CauchySeq.ma b/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
index e019be073..4bc6c7aa1 100644
--- a/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
+++ b/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
@@ -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
 *)