X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FPowerSeries.ma;h=2bb43ffc25ce7b2a4ca01ede2ea3cfc05677fa9b;hb=55444711ececb62f0a93f2a064f64c3b27f744e2;hp=de37b5e485965772df0becf9fe938765c0dacb65;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma b/helm/software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
index de37b5e48..2bb43ffc2 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/transc/PowerSeries".
 
+include "CoRN.ma".
+
 (* $Id: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *)
 
 (*#* printing Exp %\ensuremath{\exp}% *)
@@ -28,9 +30,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/PowerSeries".
 
 (*#* printing Tan %\ensuremath{\tan}% *)
 
-(* INCLUDE
-FTC
-*)
+include "ftc/FTC.ma".
 
 (*#* *More on Power Series
 
@@ -40,7 +40,7 @@ prove some important properties of these entities.
 *)
 
 (* UNEXPORTED
-Section Power_Series.
+Section Power_Series
 *)
 
 (*#* **General results
@@ -50,15 +50,15 @@ Let [a : nat -> IR].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/transc/PowerSeries/J.var.
+alias id "J" = "cic:/CoRN/transc/PowerSeries/Power_Series/J.var".
 
-inline cic:/CoRN/transc/PowerSeries/x0.var.
+alias id "x0" = "cic:/CoRN/transc/PowerSeries/Power_Series/x0.var".
 
-inline cic:/CoRN/transc/PowerSeries/Hx0.var.
+alias id "Hx0" = "cic:/CoRN/transc/PowerSeries/Power_Series/Hx0.var".
 
-inline cic:/CoRN/transc/PowerSeries/a.var.
+alias id "a" = "cic:/CoRN/transc/PowerSeries/Power_Series/a.var".
 
-inline cic:/CoRN/transc/PowerSeries/FPowerSeries.con.
+inline "cic:/CoRN/transc/PowerSeries/FPowerSeries.con".
 
 (*#*
 The most important convergence criterium specifically for power series
@@ -67,42 +67,42 @@ is the Dirichlet criterium.
 
 (* begin show *)
 
-inline cic:/CoRN/transc/PowerSeries/Ha.var.
+alias id "Ha" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha.var".
 
-inline cic:/CoRN/transc/PowerSeries/r.con.
+inline "cic:/CoRN/transc/PowerSeries/Power_Series/r.con" "Power_Series__".
 
-inline cic:/CoRN/transc/PowerSeries/Hr.con.
+inline "cic:/CoRN/transc/PowerSeries/Power_Series/Hr.con" "Power_Series__".
 
 (* end show *)
 
-inline cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con.
+inline "cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con".
 
 (*#*
 When defining a function using its Taylor series as a motivation, the following operator can be of use.
 *)
 
-inline cic:/CoRN/transc/PowerSeries/FPowerSeries'.con.
+inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'.con".
 
 (*#*
 This function is also continuous and has a good convergence ratio.
 *)
 
-inline cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con.
+inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con".
 
-inline cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con.
+inline "cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con".
 
 (* begin show *)
 
-inline cic:/CoRN/transc/PowerSeries/Ha'.var.
+alias id "Ha'" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha'.var".
 
 (* end show *)
 
-inline cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con.
+inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con".
 
-inline cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con.
+inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con".
 
 (* UNEXPORTED
-End Power_Series.
+End Power_Series
 *)
 
 (* UNEXPORTED
@@ -110,7 +110,7 @@ Hint Resolve FPowerSeries'_cont: continuous.
 *)
 
 (* UNEXPORTED
-Section More_on_PowerSeries.
+Section More_on_PowerSeries
 *)
 
 (*#*
@@ -119,31 +119,31 @@ respectively by [a] and by [fun n => (a (S n))].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/transc/PowerSeries/x0.var.
+alias id "x0" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/x0.var".
 
-inline cic:/CoRN/transc/PowerSeries/a.var.
+alias id "a" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/a.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/transc/PowerSeries/F.con.
+inline "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/F.con" "More_on_PowerSeries__".
 
-inline cic:/CoRN/transc/PowerSeries/G.con.
+inline "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/G.con" "More_on_PowerSeries__".
 
 (* end hide *)
 
 (* begin show *)
 
-inline cic:/CoRN/transc/PowerSeries/Hf.var.
+alias id "Hf" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf.var".
 
-inline cic:/CoRN/transc/PowerSeries/Hf'.var.
+alias id "Hf'" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf'.var".
 
-inline cic:/CoRN/transc/PowerSeries/Hg.var.
+alias id "Hg" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hg.var".
 
 (* end show *)
 
 (*#* We get a comparison test for power series. *)
 
-inline cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con.
+inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con".
 
 (*#* And a rule for differentiation. *)
 
@@ -151,14 +151,14 @@ inline cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con.
 Opaque nring fac.
 *)
 
-inline cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con.
+inline "cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con".
 
 (* UNEXPORTED
-End More_on_PowerSeries.
+End More_on_PowerSeries
 *)
 
 (* UNEXPORTED
-Section Definitions.
+Section Definitions
 *)
 
 (*#* **Function definitions through power series
@@ -168,58 +168,58 @@ series, and prove their convergence.  Tangent is defined as the
 quotient of sine over cosine.
 *)
 
-inline cic:/CoRN/transc/PowerSeries/Exp_ps.con.
+inline "cic:/CoRN/transc/PowerSeries/Exp_ps.con".
 
-inline cic:/CoRN/transc/PowerSeries/sin_seq.con.
+inline "cic:/CoRN/transc/PowerSeries/sin_seq.con".
 
-inline cic:/CoRN/transc/PowerSeries/sin_ps.con.
+inline "cic:/CoRN/transc/PowerSeries/sin_ps.con".
 
-inline cic:/CoRN/transc/PowerSeries/cos_seq.con.
+inline "cic:/CoRN/transc/PowerSeries/cos_seq.con".
 
-inline cic:/CoRN/transc/PowerSeries/cos_ps.con.
+inline "cic:/CoRN/transc/PowerSeries/cos_ps.con".
 
-inline cic:/CoRN/transc/PowerSeries/Exp_conv'.con.
+inline "cic:/CoRN/transc/PowerSeries/Exp_conv'.con".
 
-inline cic:/CoRN/transc/PowerSeries/Exp_conv.con.
+inline "cic:/CoRN/transc/PowerSeries/Exp_conv.con".
 
-inline cic:/CoRN/transc/PowerSeries/sin_conv.con.
+inline "cic:/CoRN/transc/PowerSeries/sin_conv.con".
 
-inline cic:/CoRN/transc/PowerSeries/cos_conv.con.
+inline "cic:/CoRN/transc/PowerSeries/cos_conv.con".
 
-inline cic:/CoRN/transc/PowerSeries/Expon.con.
+inline "cic:/CoRN/transc/PowerSeries/Expon.con".
 
-inline cic:/CoRN/transc/PowerSeries/Sine.con.
+inline "cic:/CoRN/transc/PowerSeries/Sine.con".
 
-inline cic:/CoRN/transc/PowerSeries/Cosine.con.
+inline "cic:/CoRN/transc/PowerSeries/Cosine.con".
 
-inline cic:/CoRN/transc/PowerSeries/Tang.con.
+inline "cic:/CoRN/transc/PowerSeries/Tang.con".
 
 (*#*
 Some auxiliary domain results.
 *)
 
-inline cic:/CoRN/transc/PowerSeries/Exp_domain.con.
+inline "cic:/CoRN/transc/PowerSeries/Exp_domain.con".
 
-inline cic:/CoRN/transc/PowerSeries/sin_domain.con.
+inline "cic:/CoRN/transc/PowerSeries/sin_domain.con".
 
-inline cic:/CoRN/transc/PowerSeries/cos_domain.con.
+inline "cic:/CoRN/transc/PowerSeries/cos_domain.con".
 
-inline cic:/CoRN/transc/PowerSeries/included_Exp.con.
+inline "cic:/CoRN/transc/PowerSeries/included_Exp.con".
 
-inline cic:/CoRN/transc/PowerSeries/included_Sin.con.
+inline "cic:/CoRN/transc/PowerSeries/included_Sin.con".
 
-inline cic:/CoRN/transc/PowerSeries/included_Cos.con.
+inline "cic:/CoRN/transc/PowerSeries/included_Cos.con".
 
 (*#*
 Definition of the logarithm.
 *)
 
-inline cic:/CoRN/transc/PowerSeries/log_defn_lemma.con.
+inline "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con".
 
-inline cic:/CoRN/transc/PowerSeries/Logarithm.con.
+inline "cic:/CoRN/transc/PowerSeries/Logarithm.con".
 
 (* UNEXPORTED
-End Definitions.
+End Definitions
 *)
 
 (* UNEXPORTED
@@ -230,13 +230,13 @@ Hint Resolve included_Exp included_Sin included_Cos: included.
 As most of these functions are total, it makes sense to treat them as setoid functions on the reals.  In the case of logarithm and tangent, this is not possible; however, we still define some abbreviations for aesthetical reasons.
 *)
 
-inline cic:/CoRN/transc/PowerSeries/Exp.con.
+inline "cic:/CoRN/transc/PowerSeries/Exp.con".
 
-inline cic:/CoRN/transc/PowerSeries/Sin.con.
+inline "cic:/CoRN/transc/PowerSeries/Sin.con".
 
-inline cic:/CoRN/transc/PowerSeries/Cos.con.
+inline "cic:/CoRN/transc/PowerSeries/Cos.con".
 
-inline cic:/CoRN/transc/PowerSeries/Log.con.
+inline "cic:/CoRN/transc/PowerSeries/Log.con".
 
-inline cic:/CoRN/transc/PowerSeries/Tan.con.
+inline "cic:/CoRN/transc/PowerSeries/Tan.con".