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=HEAD;hp=ffd7d47207754f24e1a5454bf3b0f3f113f8c30f;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;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 ffd7d4720..2bb43ffc2 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
@@ -40,7 +40,7 @@ prove some important properties of these entities.
 *)
 
 (* UNEXPORTED
-Section Power_Series.
+Section Power_Series
 *)
 
 (*#* **General results
@@ -50,13 +50,13 @@ 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".
 
@@ -67,11 +67,11 @@ 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 *)
 
@@ -93,7 +93,7 @@ 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 *)
 
@@ -102,7 +102,7 @@ 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,25 +119,25 @@ 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 *)
 
@@ -154,11 +154,11 @@ Opaque nring fac.
 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
@@ -219,7 +219,7 @@ inline "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con".
 inline "cic:/CoRN/transc/PowerSeries/Logarithm.con".
 
 (* UNEXPORTED
-End Definitions.
+End Definitions
 *)
 
 (* UNEXPORTED