Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / metrics / CMetricSpaces.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma b/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma
index 670bf8655fc36193e9ccdf4b5d0942e04157df4c..b0d848ec0246f831cab9ad5eb41c30b2e698503a 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma
@@ -46,11 +46,11 @@ Section MS_basics
 (*#* **Metric Space basics
 *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con" as lemma.
 
 (* UNEXPORTED
 End MS_basics
@@ -67,9 +67,9 @@ Section prodandsub
 The product of two metric spaces is again a metric space.
 *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con" as definition.
 
 (*#*
 A subspace of a metric space is again a metric space.
@@ -79,9 +79,9 @@ A subspace of a metric space is again a metric space.
 Implicit Arguments SubPsMetricSpace [X].
 *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments SubMetricSpace [X].
@@ -102,69 +102,69 @@ Section Zeroff
 Not all pseudo metric spaces are a metric space:
 *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con" as lemma.
 
 (*#*
 But a pseudo metric space induces a metric space:
 *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con" as definition.
 
 (*#*
 Some pseudo metric spaces already are a metric space:
 *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con" as definition.
 
 (*#*
 In that case the induced metric space is equivalent to the original one:
 *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Emb.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Emb.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con" as lemma.
 
 (* UNEXPORTED
 End Zeroff
@@ -187,17 +187,17 @@ Implicit Arguments MSseqLimit [X].
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/nz.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/nz.con" as lemma.
 
 (* end hide *)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_wd.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_wd.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con".
+inline procedural "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con" as lemma.
 
 (* UNEXPORTED
 End Limitt