...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / reals / Series.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma
index 3ad3ce01b943ccb59e23c75b5703c8dd6ed02f9a..80e034a8d8e5263fe4ba32e74b54c951e00e0460 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma
@@ -43,7 +43,9 @@ To each such sequence we can assign a sequence of partial sums.
 %\end{convention}%
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Definitions/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Definitions/x.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/seq_part_sum.con" as definition.
 
@@ -97,7 +99,9 @@ End Definitions
 Section More_Definitions
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/More_Definitions/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/More_Definitions/x.var
+*)
 
 (*#* We also define absolute convergence. *)
 
@@ -127,11 +131,17 @@ we can also compute its sum.
 %\end{convention}%
 *)
 
-alias id "c" = "cic:/CoRN/reals/Series/Power_Series/c.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Power_Series/c.var
+*)
 
-alias id "H0c" = "cic:/CoRN/reals/Series/Power_Series/H0c.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Power_Series/H0c.var
+*)
 
-alias id "Hc1" = "cic:/CoRN/reals/Series/Power_Series/Hc1.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Power_Series/Hc1.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/c_exp_Lim.con" as lemma.
 
@@ -166,13 +176,21 @@ of two convergent series.
 %\end{convention}%
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Operations/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/x.var
+*)
 
-alias id "y" = "cic:/CoRN/reals/Series/Operations/y.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/y.var
+*)
 
-alias id "convX" = "cic:/CoRN/reals/Series/Operations/convX.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/convX.var
+*)
 
-alias id "convY" = "cic:/CoRN/reals/Series/Operations/convY.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/convY.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/convergent_wd.con" as lemma.
 
@@ -188,7 +206,9 @@ inline procedural "cic:/CoRN/reals/Series/series_sum_minus.con" as lemma.
 
 (*#* Multiplication by a scalar [c] is also permitted. *)
 
-alias id "c" = "cic:/CoRN/reals/Series/Operations/c.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/c.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/conv_series_mult_scal.con" as lemma.
 
@@ -202,9 +222,13 @@ End Operations
 Section More_Operations
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/More_Operations/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/More_Operations/x.var
+*)
 
-alias id "convX" = "cic:/CoRN/reals/Series/More_Operations/convX.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/More_Operations/convX.var
+*)
 
 (*#* As a corollary, we get the series of the inverses. *)
 
@@ -228,13 +252,19 @@ and derive an important corollary for series.
 Let [x,y : nat->IR] be equal after some natural number.
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Almost_Everywhere/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Almost_Everywhere/x.var
+*)
 
-alias id "y" = "cic:/CoRN/reals/Series/Almost_Everywhere/y.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Almost_Everywhere/y.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/aew_eq.con" as definition.
 
-alias id "aew_equal" = "cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/aew_Cauchy.con" as lemma.
 
@@ -252,11 +282,17 @@ Section Cauchy_Almost_Everywhere
 
 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var
+*)
 
-alias id "y" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var
+*)
 
-alias id "aew_equal" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/aew_Lim.con" as lemma.
 
@@ -274,7 +310,9 @@ Section Convergence_Criteria
 %\end{convention}%
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Convergence_Criteria/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Convergence_Criteria/x.var
+*)
 
 (*#* We include the comparison test for series, both in a strong and in a less 
 general (but simpler) form.
@@ -304,7 +342,9 @@ End Convergence_Criteria
 Section More_CC
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/More_CC/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/More_CC/x.var
+*)
 
 inline procedural "cic:/CoRN/reals/Series/ratio_test_conv.con" as lemma.
 
@@ -324,13 +364,21 @@ Alternate series are a special case.  Suppose that [x] is nonnegative and
 decreasing convergent to 0.
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Alternate_Series/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Alternate_Series/x.var
+*)
 
-alias id "pos_x" = "cic:/CoRN/reals/Series/Alternate_Series/pos_x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Alternate_Series/pos_x.var
+*)
 
-alias id "Lim_x" = "cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var
+*)
 
-alias id "mon_x" = "cic:/CoRN/reals/Series/Alternate_Series/mon_x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Alternate_Series/mon_x.var
+*)
 
 (* begin hide *)