Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/NthDerivative.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/NthDerivative.mma
index a814c6fafafa6f63fd36240f0f7f56bbeed443f3..2834afd3561cd2d51c262a7cefaaff9940a94882 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/NthDerivative.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/NthDerivative.mma
@@ -48,13 +48,13 @@ alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__" as definition.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con" as definition.
 
 (*#*
 Unlike first order differentiability, for our definition to be
@@ -63,7 +63,7 @@ to be [n] times differentiable instead of quantifying over the
 [Derivative_I_n] relation.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con" as definition.
 
 (* UNEXPORTED
 End Nth_Derivative
@@ -94,19 +94,19 @@ alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__" as definition.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con" as lemma.
 
 (* UNEXPORTED
 End Trivia
@@ -132,9 +132,9 @@ alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__" as definition.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__" as definition.
 
 (* end hide *)
 
@@ -142,15 +142,15 @@ inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Resul
 We begin by showing that having a higher order derivative implies being differentiable.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con" as lemma.
 
 (*#*
 If a function is [n] times differentiable then it is also [m] times differentiable for every [m] less or equal than [n].
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con" as lemma.
 
 (*#*
 The next result consolidates our intuition that a function is [n]
@@ -158,31 +158,31 @@ times differentiable if we can build from it a chain of [n]
 derivatives.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con" as lemma.
 
 (*#*
 As expected, an [n] times differentiable in [[a,b]] function must be
 defined in that interval.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con" as lemma.
 
 (*#*
 Also, the notions of derivative and differentiability are related as expected.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con" as lemma.
 
 (*#*
 From this we can prove that if [F] has an nth order derivative in
 [[a,b]] then both [F] and its derivative are defined in that interval.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con" as lemma.
 
 (* UNEXPORTED
 Section aux
@@ -202,9 +202,9 @@ alias id "diffFn" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var".
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con" as lemma.
 
 (* UNEXPORTED
 End aux
@@ -214,15 +214,15 @@ End aux
 As usual, nth order derivability is preserved by shrinking the interval.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con" as lemma.
 
 (*#*
 And finally we have an addition rule for the order of the derivative.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con" as lemma.
 
 (* UNEXPORTED
 End Basic_Results
@@ -240,9 +240,9 @@ alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__" as definition.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__" as definition.
 
 (* end hide *)
 
@@ -254,27 +254,27 @@ elimination which we would get if we had defined nth differentiability
 as an existential quantification of the nth derivative relation.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con" as definition.
 
 (*#*
 This operator is well defined and works as expected.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con" as lemma.
 
 (*#*
 Some basic properties of this operation.
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con" as lemma.
 
 (* UNEXPORTED
 End More_Results
@@ -288,11 +288,11 @@ Section More_on_n_deriv
 Some not so basic properties of this operation (needed in rather specific situations).
 *)
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con" as lemma.
 
 (* UNEXPORTED
 End More_on_n_deriv