X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCPMSTheory.ma;h=50786005f33f637bcf1b1e2dedeb9d39df2b0552;hb=c450c3c9c829a8bd436732c939511731558d292d;hp=5875e22f4dd96c4f52ccad4e0665836f8c71dd3b;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git
diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
index 5875e22f4..50786005f 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
@@ -16,14 +16,14 @@
set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPMSTheory".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *)
include "metrics/Prod_Sub.ma".
(* UNEXPORTED
-Section lists.
+Section lists
*)
(*#* **Lists
@@ -67,11 +67,11 @@ of the list of images of elements of $l$ #l#.
inline "cic:/CoRN/metrics/CPMSTheory/map_member.con".
(* UNEXPORTED
-End lists.
+End lists
*)
(* UNEXPORTED
-Section loc_and_bound.
+Section loc_and_bound
*)
(*#* **Pseudo Metric Space theory
@@ -223,6 +223,6 @@ all points that are in some sense close to $P$#P#.
inline "cic:/CoRN/metrics/CPMSTheory/well_contained.con".
(* UNEXPORTED
-End loc_and_bound.
+End loc_and_bound
*)