X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FTaylor.ma;h=2bd2f07aa23521121103dcb823c12b639982eb96;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=e636e5518e218f827fafb1a03a7d46f786ca833d;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma index e636e5518..2bd2f07aa 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma @@ -16,18 +16,18 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Taylor". +include "CoRN.ma". + (* $Id: Taylor.v,v 1.10 2004/04/23 10:01:01 lcf Exp $ *) -(* INCLUDE -TaylorLemma -*) +include "ftc/TaylorLemma.ma". (* UNEXPORTED Opaque Min Max N_Deriv. *) (* UNEXPORTED -Section More_Taylor_Defs. +Section More_Taylor_Defs *) (*#* **General case @@ -39,60 +39,60 @@ The generalization to arbitrary intervals just needs a few more definitions. %\end{convention}% *) -inline cic:/CoRN/ftc/Taylor/I.var. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/I.var" "More_Taylor_Defs__". -inline cic:/CoRN/ftc/Taylor/pI.var. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/pI.var" "More_Taylor_Defs__". -inline cic:/CoRN/ftc/Taylor/F.var. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/F.var" "More_Taylor_Defs__". (* begin show *) -inline cic:/CoRN/ftc/Taylor/deriv_Sn.con. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/deriv_Sn.con" "More_Taylor_Defs__". (* end show *) -inline cic:/CoRN/ftc/Taylor/a.var. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/a.var" "More_Taylor_Defs__". -inline cic:/CoRN/ftc/Taylor/b.var. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/b.var" "More_Taylor_Defs__". -inline cic:/CoRN/ftc/Taylor/Ha.var. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/Ha.var" "More_Taylor_Defs__". -inline cic:/CoRN/ftc/Taylor/Hb.var. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/Hb.var" "More_Taylor_Defs__". (* begin show *) -inline cic:/CoRN/ftc/Taylor/fi.con. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/fi.con" "More_Taylor_Defs__". -inline cic:/CoRN/ftc/Taylor/funct_i.con. +inline "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/funct_i.con" "More_Taylor_Defs__". (* end show *) -inline cic:/CoRN/ftc/Taylor/Taylor_Seq'.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_Seq'.con". (* begin hide *) -inline cic:/CoRN/ftc/Taylor/TaylorB.con. +inline "cic:/CoRN/ftc/Taylor/TaylorB.con". (* end hide *) -inline cic:/CoRN/ftc/Taylor/Taylor_Rem.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_Rem.con". (* begin hide *) -inline cic:/CoRN/ftc/Taylor/Taylor_Sumx_lemma.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_Sumx_lemma.con". -inline cic:/CoRN/ftc/Taylor/Taylor_lemma_ap.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_lemma_ap.con". (* end hide *) -inline cic:/CoRN/ftc/Taylor/Taylor'.con. +inline "cic:/CoRN/ftc/Taylor/Taylor'.con". (* UNEXPORTED -End More_Taylor_Defs. +End More_Taylor_Defs *) (* UNEXPORTED -Section Taylor_Theorem. +Section Taylor_Theorem *) (*#* @@ -104,53 +104,53 @@ order up to [n] and [F'] be the nth-derivative of [F]. %\end{convention}% *) -inline cic:/CoRN/ftc/Taylor/I.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/I.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/pI.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/pI.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/F.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/F.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/n.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/n.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/f.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/f.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/goodF.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/goodF.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/goodF'.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/goodF'.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/derF.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/derF.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/F'.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/F'.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/derF'.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/derF'.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/a.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/a.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/b.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/b.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/Ha.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/Ha.var" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/Hb.var. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/Hb.var" "Taylor_Theorem__". (* begin show *) -inline cic:/CoRN/ftc/Taylor/funct_i.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/funct_i.con" "Taylor_Theorem__". -inline cic:/CoRN/ftc/Taylor/Taylor_Seq.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_Seq.con". -inline cic:/CoRN/ftc/Taylor/deriv_Sn.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_Theorem/deriv_Sn.con" "Taylor_Theorem__". (* end show *) -inline cic:/CoRN/ftc/Taylor/Taylor_aux.con. +inline "cic:/CoRN/ftc/Taylor/Taylor_aux.con". (* UNEXPORTED Transparent N_Deriv. *) -inline cic:/CoRN/ftc/Taylor/Taylor.con. +inline "cic:/CoRN/ftc/Taylor/Taylor.con". (* UNEXPORTED -End Taylor_Theorem. +End Taylor_Theorem *)