...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / FunctSeries.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSeries.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSeries.mma
index 49acbf1cfda3f12cce88a00cc33b836558757dfb..05ab51726b21ea8a34c6abaab7c17d261c560914 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSeries.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSeries.mma
@@ -51,11 +51,17 @@ defined in a compact interval.  For this, partial sums are defined and
 convergence is simply the convergence of the sequence of partial sums.
 *)
 
-alias id "a" = "cic:/CoRN/ftc/FunctSeries/Definitions/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Definitions/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/FunctSeries/Definitions/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Definitions/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Definitions/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Definitions/Hab.var
+*)
 
 (* begin hide *)
 
@@ -63,7 +69,9 @@ inline procedural "cic:/CoRN/ftc/FunctSeries/Definitions/I.con" "Definitions__"
 
 (* end hide *)
 
-alias id "f" = "cic:/CoRN/ftc/FunctSeries/Definitions/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Definitions/f.var
+*)
 
 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum.con" as definition.
 
@@ -85,7 +93,9 @@ the corresponding series.
 
 (* begin show *)
 
-alias id "H" = "cic:/CoRN/ftc/FunctSeries/Definitions/H.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Definitions/H.var
+*)
 
 (* end show *)
 
@@ -117,13 +127,21 @@ Hint Resolve fun_seq_part_sum_cont: continuous.
 Section More_Definitions
 *)
 
-alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Definitions/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Definitions/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Definitions/Hab.var
+*)
 
-alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Definitions/f.var
+*)
 
 (*#* A series can also be absolutely convergent. *)
 
@@ -142,11 +160,17 @@ Section Operations
 All of these are analogous to the properties for series of real numbers, so we won't comment much about them.
 *)
 
-alias id "a" = "cic:/CoRN/ftc/FunctSeries/Operations/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/FunctSeries/Operations/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Operations/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/Hab.var
+*)
 
 (* begin hide *)
 
@@ -166,9 +190,13 @@ inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_zero.con" as lemma.
 
 (* begin show *)
 
-alias id "f" = "cic:/CoRN/ftc/FunctSeries/Operations/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/f.var
+*)
 
-alias id "g" = "cic:/CoRN/ftc/FunctSeries/Operations/g.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/g.var
+*)
 
 (* end show *)
 
@@ -176,9 +204,13 @@ inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_convergent_wd.con" as le
 
 (* begin show *)
 
-alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Operations/convF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/convF.var
+*)
 
-alias id "convG" = "cic:/CoRN/ftc/FunctSeries/Operations/convG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/convG.var
+*)
 
 (* end show *)
 
@@ -197,11 +229,17 @@ inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_min.con" as lemma.
 %\end{convention}%
 *)
 
-alias id "c" = "cic:/CoRN/ftc/FunctSeries/Operations/c.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/c.var
+*)
 
-alias id "H" = "cic:/CoRN/ftc/FunctSeries/Operations/H.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/H.var
+*)
 
-alias id "contH" = "cic:/CoRN/ftc/FunctSeries/Operations/contH.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Operations/contH.var
+*)
 
 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_scal.con" as lemma.
 
@@ -215,11 +253,17 @@ End Operations
 Section More_Operations
 *)
 
-alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Operations/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Operations/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Operations/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Operations/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Operations/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Operations/Hab.var
+*)
 
 (* begin hide *)
 
@@ -227,9 +271,13 @@ inline procedural "cic:/CoRN/ftc/FunctSeries/More_Operations/I.con" "More_Operat
 
 (* end hide *)
 
-alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Operations/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Operations/f.var
+*)
 
-alias id "convF" = "cic:/CoRN/ftc/FunctSeries/More_Operations/convF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/More_Operations/convF.var
+*)
 
 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_inv.con" as lemma.
 
@@ -243,15 +291,25 @@ End More_Operations
 Section Other_Results
 *)
 
-alias id "a" = "cic:/CoRN/ftc/FunctSeries/Other_Results/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Other_Results/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/FunctSeries/Other_Results/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Other_Results/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Other_Results/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Other_Results/Hab.var
+*)
 
-alias id "f" = "cic:/CoRN/ftc/FunctSeries/Other_Results/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Other_Results/f.var
+*)
 
-alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Other_Results/convF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Other_Results/convF.var
+*)
 
 (*#*
 The following relate the sum series with the limit of the sequence of
@@ -286,11 +344,17 @@ Section Convergence_Criteria
 Most of the convergence criteria for series of real numbers carry over to series of real-valued functions, so again we just present them without comments.
 *)
 
-alias id "a" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/Hab.var
+*)
 
 (* begin hide *)
 
@@ -298,9 +362,13 @@ inline procedural "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/I.con" "Conver
 
 (* end hide *)
 
-alias id "f" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/f.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/contF.var
+*)
 
 (* UNEXPORTED
 Opaque Frestr.