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
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 *)
inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con".
(* UNEXPORTED
-End Nth_Derivative.
+End Nth_Derivative
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Trivia.
+Section Trivia
*)
(*#* **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 *)
inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con".
(* UNEXPORTED
-End Trivia.
+End Trivia
*)
(* UNEXPORTED
-Section Basic_Results.
+Section Basic_Results
*)
(*#* **Basic Results
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 *)
inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con".
(* UNEXPORTED
-Section aux.
+Section aux
*)
(*#*
(* 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 *)
inline "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con".
(* UNEXPORTED
-End aux.
+End aux
*)
(*#*
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 *)
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
*)
(*#*
inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con".
(* UNEXPORTED
-End More_on_n_deriv.
+End More_on_n_deriv
*)