X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FProd_Sub.ma;h=f30b3c65d7f6038f88d9f7f03650e50430cab8aa;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=c1a6e78edf701b6ee2cdebaecd6dd9e7d89192ff;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
index c1a6e78ed..f30b3c65d 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
@@ -16,11 +16,11 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/metrics/Prod_Sub".
 
+include "CoRN.ma".
+
 (* $Id: Prod_Sub.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
 
-(* INCLUDE
-IR_CPMSpace
-*)
+include "metrics/IR_CPMSpace.ma".
 
 (* UNEXPORTED
 Section prodpsmetrics.
@@ -37,15 +37,15 @@ This is %\emph{not}% #<I>not</I># the one used to make the metric of
 $\RR^{2}$ #IR<SUP>2</SUP># out of the metric of $\RR$ #IR#. 
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/dprod0.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dprod0.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/dprod0_strext.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dprod0_strext.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/d_prod0.con.
+inline "cic:/CoRN/metrics/Prod_Sub/d_prod0.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/prod0cpsmetricspace_is_CPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/prod0cpsmetricspace_is_CPsMetricSpace.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/Prod0CPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/Prod0CPsMetricSpace.con".
 
 (* UNEXPORTED
 End prodpsmetrics.
@@ -63,45 +63,45 @@ The pseudo metric on a subspace $Y$ #Y# of a pseudo metric space $X$ #X# is
 the pseudo metric on $X$ #X# restricted to $Y$ #Y#.
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/restr_bin_fun.con.
+inline "cic:/CoRN/metrics/Prod_Sub/restr_bin_fun.con".
 
 (* UNEXPORTED
 Implicit Arguments restr_bin_fun [X].
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/restr_bin_fun'.con.
+inline "cic:/CoRN/metrics/Prod_Sub/restr_bin_fun'.con".
 
 (* UNEXPORTED
 Implicit Arguments restr_bin_fun' [X].
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/restr_bin_fun_strext.con.
+inline "cic:/CoRN/metrics/Prod_Sub/restr_bin_fun_strext.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/Build_SubCSetoid_bin_fun.con.
+inline "cic:/CoRN/metrics/Prod_Sub/Build_SubCSetoid_bin_fun.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub.con".
 
 (* UNEXPORTED
 Implicit Arguments dsub [X].
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub_com.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_com.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub_nneg.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_nneg.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub_pos_imp_ap.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_pos_imp_ap.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub_tri_ineq.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_tri_ineq.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/is_SubPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/is_SubPsMetricSpace.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/SubPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/SubPsMetricSpace.con".
 
 (* UNEXPORTED
 Implicit Arguments SubPsMetricSpace [X].
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/from_SubPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/from_SubPsMetricSpace.con".
 
 (*#*
 The function [dsub'] is used in the definition of %''located''% #"located"#. 
@@ -109,21 +109,21 @@ It enables one to speak about a distance between an element of a
 pseudo metric space and a certain subspace.
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub'.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'.con".
 
 (* UNEXPORTED
 Implicit Arguments dsub' [X].
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub'_strext.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'_strext.con".
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub'_as_cs_fun.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'_as_cs_fun.con".
 
 (* UNEXPORTED
 Implicit Arguments dsub'_as_cs_fun [X].
 *)
 
-inline cic:/CoRN/metrics/Prod_Sub/dsub'_uni_continuous''.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'_uni_continuous''.con".
 
 (* UNEXPORTED
 End subpsmetrics.