X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FNthDerivative.ma;h=180d8a7a2406c909671be36648e71de6e1ba70e0;hb=11a6c88f3e717b019be2eae71711c70473b5467a;hp=bd2735e2f9b0ae4de221f59755a134b4072d63f4;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma index bd2735e2f..180d8a7a2 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma @@ -16,14 +16,14 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/NthDerivative". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *) include "ftc/Differentiability.ma". (* UNEXPORTED -Section Nth_Derivative. +Section Nth_Derivative *) (*#* *Nth Derivative @@ -42,17 +42,17 @@ We now study higher order differentiability. We first define what we mean by the derivative of order [n] of a function. *) -inline "cic:/CoRN/ftc/NthDerivative/a.var". +alias id "a" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var". -inline "cic:/CoRN/ftc/NthDerivative/b.var". +alias id "b" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var". -inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var". (* begin hide *) -inline "cic:/CoRN/ftc/NthDerivative/Hab.con". +inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__". -inline "cic:/CoRN/ftc/NthDerivative/I.con". +inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__". (* end hide *) @@ -68,7 +68,7 @@ to be [n] times differentiable instead of quantifying over the inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con". (* UNEXPORTED -End Nth_Derivative. +End Nth_Derivative *) (* UNEXPORTED @@ -80,7 +80,7 @@ Implicit Arguments Diffble_I_n [a b]. *) (* UNEXPORTED -Section Trivia. +Section Trivia *) (*#* **Trivia @@ -88,17 +88,17 @@ Section Trivia. These are the expected extensionality and uniqueness results. *) -inline "cic:/CoRN/ftc/NthDerivative/a.var". +alias id "a" = "cic:/CoRN/ftc/NthDerivative/Trivia/a.var". -inline "cic:/CoRN/ftc/NthDerivative/b.var". +alias id "b" = "cic:/CoRN/ftc/NthDerivative/Trivia/b.var". -inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var". (* begin hide *) -inline "cic:/CoRN/ftc/NthDerivative/Hab.con". +inline "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__". -inline "cic:/CoRN/ftc/NthDerivative/I.con". +inline "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__". (* end hide *) @@ -111,11 +111,11 @@ inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con". inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con". (* UNEXPORTED -End Trivia. +End Trivia *) (* UNEXPORTED -Section Basic_Results. +Section Basic_Results *) (*#* **Basic Results @@ -126,17 +126,17 @@ the relation of [n] times derivative, but focus rather on the definition of [Diffble_I_n]. *) -inline "cic:/CoRN/ftc/NthDerivative/a.var". +alias id "a" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var". -inline "cic:/CoRN/ftc/NthDerivative/b.var". +alias id "b" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var". -inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var". (* begin hide *) -inline "cic:/CoRN/ftc/NthDerivative/Hab.con". +inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__". -inline "cic:/CoRN/ftc/NthDerivative/I.con". +inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__". (* end hide *) @@ -187,7 +187,7 @@ inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con". inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con". (* UNEXPORTED -Section aux. +Section aux *) (*#* @@ -196,11 +196,11 @@ First order differentiability is just a special case. (* begin show *) -inline "cic:/CoRN/ftc/NthDerivative/F.var". +alias id "F" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var". -inline "cic:/CoRN/ftc/NthDerivative/diffF.var". +alias id "diffF" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var". -inline "cic:/CoRN/ftc/NthDerivative/diffFn.var". +alias id "diffFn" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var". (* end show *) @@ -209,7 +209,7 @@ inline "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con". inline "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con". (* UNEXPORTED -End aux. +End aux *) (*#* @@ -227,24 +227,24 @@ And finally we have an addition rule for the order of the derivative. inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con". (* UNEXPORTED -End Basic_Results. +End Basic_Results *) (* UNEXPORTED -Section More_Results. +Section More_Results *) -inline "cic:/CoRN/ftc/NthDerivative/a.var". +alias id "a" = "cic:/CoRN/ftc/NthDerivative/More_Results/a.var". -inline "cic:/CoRN/ftc/NthDerivative/b.var". +alias id "b" = "cic:/CoRN/ftc/NthDerivative/More_Results/b.var". -inline "cic:/CoRN/ftc/NthDerivative/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var". (* begin hide *) -inline "cic:/CoRN/ftc/NthDerivative/Hab.con". +inline "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__". -inline "cic:/CoRN/ftc/NthDerivative/I.con". +inline "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__". (* end hide *) @@ -279,11 +279,11 @@ inline "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con". inline "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con". (* UNEXPORTED -End More_Results. +End More_Results *) (* UNEXPORTED -Section More_on_n_deriv. +Section More_on_n_deriv *) (*#* @@ -297,6 +297,6 @@ inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con". inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con". (* UNEXPORTED -End More_on_n_deriv. +End More_on_n_deriv *)