made executable again

[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..504a7d7a064111f114f4d29d9c6a365a65b15969 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
@@ -16,14 +16,14 @@
 
 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.
+Section Continuous_functions
 *)
 
 (*#* **Continuous functions, uniformly continuous functions and Lipschitz functions
@@ -32,30 +32,30 @@ Let [A] and [B] be pseudo metric spaces.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/A.var.
+alias id "A" = "cic:/CoRN/metrics/ContFunctions/Continuous_functions/A.var".
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Continuous_functions/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.
+End Continuous_functions
 *)
 
 (* UNEXPORTED
@@ -87,44 +87,44 @@ Implicit Arguments lipschitz' [A B].
 *)
 
 (* UNEXPORTED
-Section Lemmas.
+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.
+End Lemmas
 *)
 
 (* UNEXPORTED
-Section Identity.
+Section Identity
 *)
 
 (*#* **Identity 
@@ -135,18 +135,18 @@ 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.
+End Identity
 *)
 
 (* UNEXPORTED
-Section Constant.
+Section Constant
 *)
 
 (*#* **Constant functions
@@ -160,22 +160,22 @@ Any constant function is Lipschitz.
 Hence it is uniformly continuous and continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Constant/B.var".
 
-inline cic:/CoRN/metrics/ContFunctions/X.var.
+alias id "X" = "cic:/CoRN/metrics/ContFunctions/Constant/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.
+End Constant
 *)
 
 (* UNEXPORTED
-Section Composition.
+Section Composition
 *)
 
 (*#* **Composition
@@ -191,58 +191,58 @@ The composition of two Lipschitz/uniformly continous/continuous functions is
 again Lipschitz/uniformly continuous/continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/X.var.
+alias id "X" = "cic:/CoRN/metrics/ContFunctions/Composition/X.var".
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Composition/B.var".
 
-inline cic:/CoRN/metrics/ContFunctions/f.var.
+alias id "f" = "cic:/CoRN/metrics/ContFunctions/Composition/f.var".
 
-inline cic:/CoRN/metrics/ContFunctions/C.var.
+alias id "C" = "cic:/CoRN/metrics/ContFunctions/Composition/C.var".
 
-inline cic:/CoRN/metrics/ContFunctions/g.var.
+alias id "g" = "cic:/CoRN/metrics/ContFunctions/Composition/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.
+End Composition
 *)
 
 (* UNEXPORTED
-Section Limit.
+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.
+End Limit
 *)