X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FTaylorSeries.ma;h=7e00f92c8cfdca1801b8a8f725ecc873cd56a9bc;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=74966e1d9345f30ee3a29645e33b77216e741888;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma b/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma index 74966e1d9..7e00f92c8 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma @@ -40,20 +40,20 @@ point of [J]. *) (* UNEXPORTED -Section Definitions. +Section Definitions *) -inline "cic:/CoRN/transc/TaylorSeries/J.var". +alias id "J" = "cic:/CoRN/transc/TaylorSeries/Definitions/J.var". -inline "cic:/CoRN/transc/TaylorSeries/pJ.var". +alias id "pJ" = "cic:/CoRN/transc/TaylorSeries/Definitions/pJ.var". -inline "cic:/CoRN/transc/TaylorSeries/F.var". +alias id "F" = "cic:/CoRN/transc/TaylorSeries/Definitions/F.var". -inline "cic:/CoRN/transc/TaylorSeries/diffF.var". +alias id "diffF" = "cic:/CoRN/transc/TaylorSeries/Definitions/diffF.var". -inline "cic:/CoRN/transc/TaylorSeries/a.var". +alias id "a" = "cic:/CoRN/transc/TaylorSeries/Definitions/a.var". -inline "cic:/CoRN/transc/TaylorSeries/Ha.var". +alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Definitions/Ha.var". inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con". @@ -63,9 +63,9 @@ derivatives of [F]. %\end{convention}% *) -inline "cic:/CoRN/transc/TaylorSeries/f.var". +alias id "f" = "cic:/CoRN/transc/TaylorSeries/Definitions/f.var". -inline "cic:/CoRN/transc/TaylorSeries/derF.var". +alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Definitions/derF.var". inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series.con". @@ -80,11 +80,11 @@ inline "cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con". inline "cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con". (* UNEXPORTED -End Definitions. +End Definitions *) (* UNEXPORTED -Section Convergence_in_IR. +Section Convergence_in_IR *) (*#* **Convergence @@ -95,17 +95,17 @@ derivatives of [F] that guarantees convergence of its Taylor series to [F]. *) -inline "cic:/CoRN/transc/TaylorSeries/H.var". +alias id "H" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H.var". -inline "cic:/CoRN/transc/TaylorSeries/F.var". +alias id "F" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/F.var". -inline "cic:/CoRN/transc/TaylorSeries/a.var". +alias id "a" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/a.var". -inline "cic:/CoRN/transc/TaylorSeries/Ha.var". +alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Ha.var". -inline "cic:/CoRN/transc/TaylorSeries/f.var". +alias id "f" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/f.var". -inline "cic:/CoRN/transc/TaylorSeries/derF.var". +alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/derF.var". inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con". @@ -115,7 +115,7 @@ inline "cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con". (* begin show *) -inline "cic:/CoRN/transc/TaylorSeries/bndf.var". +alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/bndf.var". (* end show *) @@ -125,7 +125,7 @@ Opaque nexp_op fac. (* begin hide *) -inline "cic:/CoRN/transc/TaylorSeries/H1.con". +inline "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H1.con" "Convergence_in_IR__". (* UNEXPORTED Transparent nexp_op. @@ -173,7 +173,7 @@ will separately assume convergence. (* begin show *) -inline "cic:/CoRN/transc/TaylorSeries/Hf.var". +alias id "Hf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Hf.var". (* end show *) @@ -188,11 +188,11 @@ Opaque mult. inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con". (* UNEXPORTED -End Convergence_in_IR. +End Convergence_in_IR *) (* UNEXPORTED -Section Other_Results. +Section Other_Results *) (*#* @@ -220,39 +220,39 @@ provided that their derivatives coincide at a given point and their Taylor series converge to themselves. *) -inline "cic:/CoRN/transc/TaylorSeries/F.var". +alias id "F" = "cic:/CoRN/transc/TaylorSeries/Other_Results/F.var". -inline "cic:/CoRN/transc/TaylorSeries/G.var". +alias id "G" = "cic:/CoRN/transc/TaylorSeries/Other_Results/G.var". -inline "cic:/CoRN/transc/TaylorSeries/a.var". +alias id "a" = "cic:/CoRN/transc/TaylorSeries/Other_Results/a.var". -inline "cic:/CoRN/transc/TaylorSeries/f.var". +alias id "f" = "cic:/CoRN/transc/TaylorSeries/Other_Results/f.var". -inline "cic:/CoRN/transc/TaylorSeries/g.var". +alias id "g" = "cic:/CoRN/transc/TaylorSeries/Other_Results/g.var". -inline "cic:/CoRN/transc/TaylorSeries/derF.var". +alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derF.var". -inline "cic:/CoRN/transc/TaylorSeries/derG.var". +alias id "derG" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derG.var". -inline "cic:/CoRN/transc/TaylorSeries/bndf.var". +alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndf.var". -inline "cic:/CoRN/transc/TaylorSeries/bndg.var". +alias id "bndg" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndg.var". (* begin show *) -inline "cic:/CoRN/transc/TaylorSeries/Heq.var". +alias id "Heq" = "cic:/CoRN/transc/TaylorSeries/Other_Results/Heq.var". (* end show *) (* begin hide *) -inline "cic:/CoRN/transc/TaylorSeries/Hf.con". +inline "cic:/CoRN/transc/TaylorSeries/Other_Results/Hf.con" "Other_Results__". (* end hide *) inline "cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con". (* UNEXPORTED -End Other_Results. +End Other_Results *)