Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / Composition.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma
index 2d2ebfbabbecc99b2ce9653ffc81896c399359c5..7fa209cee4acb8146519d16e42098ed2d6db3551 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma
@@ -69,7 +69,7 @@ alias id "Hcd" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.va
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__".
+inline procedural "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__" as definition.
 
 (* end hide *)
 
@@ -79,7 +79,7 @@ alias id "Hf" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var"
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_into_compacts.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_into_compacts.con" as definition.
 
 (* begin show *)
 
@@ -87,13 +87,13 @@ alias id "maps" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/maps.
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma'.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_less.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_less.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_inc.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_inc.con" as lemma.
 
 (* UNEXPORTED
 End Part_Funct
@@ -138,7 +138,7 @@ alias id "maps" = "cic:/CoRN/ftc/Composition/Mapping/maps.var".
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/included_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/included_comp.con" as lemma.
 
 (* UNEXPORTED
 End Mapping
@@ -161,7 +161,7 @@ alias id "Hab" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__".
+inline procedural "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__" as definition.
 
 (* end hide *)
 
@@ -185,7 +185,7 @@ alias id "Hmap" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var".
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Continuous_I_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Continuous_I_comp.con" as lemma.
 
 (* UNEXPORTED
 End Interval_Continuity
@@ -222,11 +222,11 @@ alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Derivative/Hcd'.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__" as definition.
 
 (* end hide *)
 
@@ -240,17 +240,17 @@ alias id "Hmap" = "cic:/CoRN/ftc/Composition/Derivative/Hmap.var".
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/included_comp'.con".
+inline procedural "cic:/CoRN/ftc/Composition/included_comp'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps'.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative_I_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative_I_comp.con" as lemma.
 
 (*#*
 The next lemma will be useful when we move on to differentiability.
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con".
+inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con" as lemma.
 
 (* UNEXPORTED
 End Derivative
@@ -283,11 +283,11 @@ alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__".
+inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__".
+inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__".
+inline procedural "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__" as definition.
 
 (* end hide *)
 
@@ -301,7 +301,7 @@ alias id "Hmap" = "cic:/CoRN/ftc/Composition/Differentiability/Hmap.var".
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp.con" as lemma.
 
 (* UNEXPORTED
 End Differentiability
@@ -327,13 +327,13 @@ alias id "pI" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var".
 
 alias id "pJ" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var".
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_compacts_into.con" as definition.
 
 (*#*
 Now everything comes naturally:
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/comp_inc_lemma.con".
+inline procedural "cic:/CoRN/ftc/Composition/comp_inc_lemma.con" as lemma.
 
 alias id "F" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var".
 
@@ -349,7 +349,7 @@ alias id "Hmap" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var".
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Continuous_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Continuous_comp.con" as lemma.
 
 (* begin show *)
 
@@ -357,7 +357,7 @@ alias id "Hmap'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap'.var".
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative_comp.con" as lemma.
 
 (* UNEXPORTED
 End Generalized_Intervals
@@ -371,21 +371,21 @@ Section Corollaries
 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/positive_fun.con".
+inline procedural "cic:/CoRN/ftc/Composition/positive_fun.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/negative_fun.con".
+inline procedural "cic:/CoRN/ftc/Composition/negative_fun.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con" as lemma.
 
 (*#*
 As a corollary, we get the generalization of differentiability property.
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Diffble_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Diffble_comp.con" as lemma.
 
 (* UNEXPORTED
 End Corollaries