- transcript: now outputs includes and coercions correctly

[helm.git] / helm / software / matita / contribs / CoRN-Decl / metrics / ContFunctions.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
index b4fa706898f738223f65cab96de232d6827f79c1..0f93560af85b96a0b0af98882fd54ba9fe725303 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
@@ -16,11 +16,11 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/metrics/ContFunctions".
 
+include "CoRN.ma".
+
 (* $Id: ContFunctions.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
 
-(* INCLUDE
-CPseudoMSpaces
-*)
+include "metrics/CPseudoMSpaces.ma".
 
 (* UNEXPORTED
 Section Continuous_functions.
@@ -32,27 +32,27 @@ Let [A] and [B] be pseudo metric spaces.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/A.var.
+inline "cic:/CoRN/metrics/ContFunctions/A.var".
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+inline "cic:/CoRN/metrics/ContFunctions/B.var".
 
 (*#*
 We will look at some notions of continuous functions.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous''.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous''.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz'.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz'.con".
 
 (* UNEXPORTED
 End Continuous_functions.
@@ -92,32 +92,32 @@ Section Lemmas.
 
 (* begin hide *)
 
-inline cic:/CoRN/metrics/ContFunctions/nexp_power.con.
+inline "cic:/CoRN/metrics/ContFunctions/nexp_power.con".
 
 (* end hide *)
 
-inline cic:/CoRN/metrics/ContFunctions/continuous_imp_continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous_imp_continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/continuous'_imp_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous'_imp_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_uni_continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_uni_continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous''.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous''.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz_imp_lipschitz'.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_lipschitz'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz'_imp_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz'_imp_lipschitz.con".
 
 (*#*
 Every uniformly continuous function is continuous and 
 every Lipschitz function is uniformly continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz_imp_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_uni_continuous.con".
 
 (* UNEXPORTED
 End Lemmas.
@@ -135,11 +135,11 @@ The identity function is Lipschitz.
 Hence it is uniformly continuous and continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/id_is_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/id_is_lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/id_is_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/id_is_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/id_is_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/id_is_continuous.con".
 
 (* UNEXPORTED
 End Identity.
@@ -160,15 +160,15 @@ Any constant function is Lipschitz.
 Hence it is uniformly continuous and continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+inline "cic:/CoRN/metrics/ContFunctions/B.var".
 
-inline cic:/CoRN/metrics/ContFunctions/X.var.
+inline "cic:/CoRN/metrics/ContFunctions/X.var".
 
-inline cic:/CoRN/metrics/ContFunctions/const_fun_is_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/const_fun_is_lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/const_fun_is_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/const_fun_is_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/const_fun_is_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/const_fun_is_continuous.con".
 
 (* UNEXPORTED
 End Constant.
@@ -191,21 +191,21 @@ The composition of two Lipschitz/uniformly continous/continuous functions is
 again Lipschitz/uniformly continuous/continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/X.var.
+inline "cic:/CoRN/metrics/ContFunctions/X.var".
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+inline "cic:/CoRN/metrics/ContFunctions/B.var".
 
-inline cic:/CoRN/metrics/ContFunctions/f.var.
+inline "cic:/CoRN/metrics/ContFunctions/f.var".
 
-inline cic:/CoRN/metrics/ContFunctions/C.var.
+inline "cic:/CoRN/metrics/ContFunctions/C.var".
 
-inline cic:/CoRN/metrics/ContFunctions/g.var.
+inline "cic:/CoRN/metrics/ContFunctions/g.var".
 
-inline cic:/CoRN/metrics/ContFunctions/comp_resp_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/comp_resp_lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/comp_resp_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/comp_resp_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/comp_resp_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/comp_resp_continuous.con".
 
 (* UNEXPORTED
 End Composition.
@@ -218,29 +218,29 @@ Section Limit.
 (*#* **Limit
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit.con".
 
 (* UNEXPORTED
 Implicit Arguments MSseqLimit [X].
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit'.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit'.con".
 
 (* UNEXPORTED
 Implicit Arguments MSseqLimit' [X].
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit_imp_MSseqLimit'.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit_imp_MSseqLimit'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit'_imp_MSseqLimit.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit'_imp_MSseqLimit.con".
 
-inline cic:/CoRN/metrics/ContFunctions/seqcontinuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/seqcontinuous'.con".
 
 (* UNEXPORTED
 Implicit Arguments seqcontinuous' [A B].
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/continuous'_imp_seqcontinuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous'_imp_seqcontinuous'.con".
 
 (* UNEXPORTED
 End Limit.