Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/metrics/CPMSTheory.mma b/helm/software/matita/contribs/CoRN-Procedural/metrics/CPMSTheory.mma
index 24b6b8bb0a2eb27dea6e80c4c1f0a12cf126d708..04afb43c8bdd005a065d68f6e96fd154f4d819a6 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/metrics/CPMSTheory.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/metrics/CPMSTheory.mma
@@ -35,19 +35,19 @@ finite sets of representants, instead of finite subsetoids. This seems to make
  the proofs a bit easier.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/MSmember.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/MSmember.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments MSmember [X].
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/to_IR.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/to_IR.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/from_IR.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/from_IR.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/list_IR.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/list_IR.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/is_P.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/is_P.con" as lemma.
 
 (*#*
 If a real number is element of a list in the above defined sense,
@@ -55,14 +55,14 @@ it is an element of the list in the sense of [member],
 that uses the setoid equality.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/member1.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/member1.con" as lemma.
 
 (*#*
 The image under a certain mapping of an element of a list $l$ #<I>l</I># is member 
 of the list of images of elements of $l$ #<I>l</I>#.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member.con" as lemma.
 
 (* UNEXPORTED
 End lists
@@ -75,13 +75,13 @@ Section loc_and_bound
 (*#* **Pseudo Metric Space theory
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con" as lemma.
 
 (* UNEXPORTED
 Implicit Arguments MSmember [X].
@@ -92,11 +92,11 @@ Again we see that the image under a certain mapping of an element of a list $l$
 #<I>l</I># is member of the list of images of elements of $l$ #<I>l</I>#.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member'.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member'.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/bounded.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/bounded.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con" as definition.
 
 (*#*
 Total boundedness is preserved under uniformly continuous mappings.
@@ -106,18 +106,18 @@ Total boundedness is preserved under uniformly continuous mappings.
 Implicit Arguments SubPsMetricSpace [X].
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con" as lemma.
 
 (*#*
 Every image under an uniformly continuous function of an totally bounded 
 pseudo metric space has an infimum and a supremum.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/infimum_exists.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/infimum_exists.con" as lemma.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/supremum_exists.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/supremum_exists.con" as lemma.
 
 (*#*
 A subspace $P$#<I>P</I># of a pseudo metric space $X$#<I>X</I># is said to be located if for all 
@@ -129,25 +129,25 @@ between $x$#<I>x</I># and the elements of $P$#<I>P</I>#.
 Implicit Arguments dsub'_as_cs_fun [X].
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/located.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/located.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments located [X].
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/located'.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/located'.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments located' [X].
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con" as lemma.
 
 (*#*
 Every totally bounded pseudo metric space is located.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con" as lemma.
 
 (*#*
 For all $x$#<I>x</I># in a pseudo metric space $X$#<I>X</I>#, for all located subspaces $P$#<I>P</I># of $X$#<I>X</I>#,
@@ -158,9 +158,9 @@ $d(x,y)\leq \mbox{inf}\{d(x,p)|p \in P\}+(n+1)^{-1}$
 one to use the latter as an argument of [map].
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/Floc.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/Floc.con" as definition.
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/Flocfun.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/Flocfun.con" as definition.
 
 (*#*
 A located subset $P$#<I>P</I># of a totally bounded pseudo metric space $X$
@@ -168,33 +168,33 @@ A located subset $P$#<I>P</I># of a totally bounded pseudo metric space $X$
 bounded.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con" as lemma.
 
 (*#*
 Here are some definitions that could come in handy:
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments MSseqLimit' [X].
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/MSComplete.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/MSComplete.con" as definition.
 
 (*#*
 A compact pseudo metric space is a pseudo metric space which is complete and 
 totally bounded.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCompact.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCompact.con" as definition.
 
 (*#*
 A subset $P$#<I>P</I># is %\emph{open}%#<I>open</I># if for all $x$#<I>x</I># in $P$#<I>P</I># there exists an open sphere 
 with centre $x$#<I>x</I># that is contained in $P$#<I>P</I>#.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/open.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/open.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments open [X].
@@ -206,7 +206,7 @@ element $x$#<I>x</I># of a located pseudo metric space $X$#<I>X</I># and the ele
 subspace $P$#<I>P</I># of $X$#<I>X</I>#.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/infima.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/infima.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments infima [X].
@@ -218,7 +218,7 @@ A non-empty totally bounded sub-pseudo-metric-space $P$#<I>P</I># is said to be
 all points that are in some sense close to $P$#<I>P</I>#.
 *)
 
-inline procedural "cic:/CoRN/metrics/CPMSTheory/well_contained.con".
+inline procedural "cic:/CoRN/metrics/CPMSTheory/well_contained.con" as definition.
 
 (* UNEXPORTED
 End loc_and_bound