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
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
inline "cic:/CoRN/metrics/CPMSTheory/well_contained.con".
(* UNEXPORTED
-End loc_and_bound.
+End loc_and_bound
*)