X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FContFunctions.ma;h=504a7d7a064111f114f4d29d9c6a365a65b15969;hb=810db29f760117d933ee1f74328043b8fce43847;hp=3fe1765efcca6d08fe6cd71c4c603dd909ee5e2c;hpb=62596f4e0a109e43c9df5da20571827c8b905ce4;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma b/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
index 3fe1765ef..504a7d7a0 100644
--- a/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
+++ b/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
@@ -32,9 +32,9 @@ Let [A] and [B] be pseudo metric spaces.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/metrics/ContFunctions/Continuous_functions/A.var" "Continuous_functions__".
+alias id "A" = "cic:/CoRN/metrics/ContFunctions/Continuous_functions/A.var".
 
-inline "cic:/CoRN/metrics/ContFunctions/Continuous_functions/B.var" "Continuous_functions__".
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Continuous_functions/B.var".
 
 (*#*
 We will look at some notions of continuous functions.
@@ -160,9 +160,9 @@ Any constant function is Lipschitz.
 Hence it is uniformly continuous and continuous.
 *)
 
-inline "cic:/CoRN/metrics/ContFunctions/Constant/B.var" "Constant__".
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Constant/B.var".
 
-inline "cic:/CoRN/metrics/ContFunctions/Constant/X.var" "Constant__".
+alias id "X" = "cic:/CoRN/metrics/ContFunctions/Constant/X.var".
 
 inline "cic:/CoRN/metrics/ContFunctions/const_fun_is_lipschitz.con".
 
@@ -191,15 +191,15 @@ The composition of two Lipschitz/uniformly continous/continuous functions is
 again Lipschitz/uniformly continuous/continuous.
 *)
 
-inline "cic:/CoRN/metrics/ContFunctions/Composition/X.var" "Composition__".
+alias id "X" = "cic:/CoRN/metrics/ContFunctions/Composition/X.var".
 
-inline "cic:/CoRN/metrics/ContFunctions/Composition/B.var" "Composition__".
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Composition/B.var".
 
-inline "cic:/CoRN/metrics/ContFunctions/Composition/f.var" "Composition__".
+alias id "f" = "cic:/CoRN/metrics/ContFunctions/Composition/f.var".
 
-inline "cic:/CoRN/metrics/ContFunctions/Composition/C.var" "Composition__".
+alias id "C" = "cic:/CoRN/metrics/ContFunctions/Composition/C.var".
 
-inline "cic:/CoRN/metrics/ContFunctions/Composition/g.var" "Composition__".
+alias id "g" = "cic:/CoRN/metrics/ContFunctions/Composition/g.var".
 
 inline "cic:/CoRN/metrics/ContFunctions/comp_resp_lipschitz.con".