- transcript: patched to generate aliases instead of inlined variables

[helm.git] / matita / contribs / CoRN-Decl / ftc / MoreFunctions.ma

diff --git a/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma b/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
index 71333c0bd57b5c54447a4c2aca03940c51895f95..4d7622ba2318fe4ae14baa440efc243b20854a5c 100644 (file)
--- a/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
+++ b/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
@@ -29,7 +29,7 @@ Opaque Min Max.
 *)
 
 (* UNEXPORTED
-Section Basic_Results.
+Section Basic_Results
 *)
 
 (*#* *More about Functions
@@ -44,7 +44,7 @@ arbitrary intervals.
 **Continuity
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var".
 
 (*#*
 Trivial stuff.
@@ -57,17 +57,17 @@ inline "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con".
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/cI.var".
+alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/Hinc.var".
+alias id "Hinc" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var".
 
 (* end show *)
 
@@ -78,7 +78,7 @@ inline "cic:/CoRN/ftc/MoreFunctions/FNorm.con".
 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con".
 
 (* UNEXPORTED
-End Basic_Results.
+End Basic_Results
 *)
 
 (* UNEXPORTED
@@ -86,26 +86,26 @@ Hint Resolve Continuous_imp_inc: included.
 *)
 
 (* UNEXPORTED
-Section Other_Results.
+Section Other_Results
 *)
 
 (*#*
 The usual stuff.
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G.var".
+alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/contG.var".
+alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var".
 
 (* end show *)
 
@@ -134,7 +134,7 @@ inline "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con".
 
 (* UNEXPORTED
-End Other_Results.
+End Other_Results
 *)
 
 (* UNEXPORTED
@@ -148,27 +148,27 @@ Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
 *)
 
 (* UNEXPORTED
-Section Corollaries.
+Section Corollaries
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/cI.var".
+alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G.var".
+alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/contG.var".
+alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con".
 
 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con".
 
 (* UNEXPORTED
-End Corollaries.
+End Corollaries
 *)
 
 (* UNEXPORTED
@@ -176,10 +176,10 @@ Hint Resolve Continuous_div: continuous.
 *)
 
 (* UNEXPORTED
-Section Sums.
+Section Sums
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Sums/I.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con".
 
@@ -188,16 +188,16 @@ inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con".
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/f.var".
+alias id "f" = "cic:/CoRN/ftc/MoreFunctions/Sums/f.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Sums/contF.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con".
 
 (* UNEXPORTED
-End Sums.
+End Sums
 *)
 
 (* UNEXPORTED
@@ -205,7 +205,7 @@ Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous.
 *)
 
 (* UNEXPORTED
-Section Basic_Properties.
+Section Basic_Properties
 *)
 
 (*#* **Derivative
@@ -216,15 +216,15 @@ Derivative is not that much different.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
+alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G.var".
+alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/H.var".
+alias id "H" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con".
 
@@ -241,7 +241,7 @@ inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con".
 
 (* UNEXPORTED
-End Basic_Properties.
+End Basic_Properties
 *)
 
 (* UNEXPORTED
@@ -254,29 +254,29 @@ Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
 *)
 
 (* UNEXPORTED
-Section More_Results.
+Section More_Results
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Results/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
+alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var".
 
 (*#*
 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F'.var".
+alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G.var".
+alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G'.var".
+alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/derF.var".
+alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/derG.var".
+alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con".
 
@@ -301,58 +301,58 @@ inline "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con".
 
 (* UNEXPORTED
-End More_Results.
+End More_Results
 *)
 
 (* UNEXPORTED
-Section More_Corollaries.
+Section More_Corollaries
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
+alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F'.var".
+alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G.var".
+alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G'.var".
+alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/derF.var".
+alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/derG.var".
+alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/Gbnd.var".
+alias id "Gbnd" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var".
 
 (* end show *)
 
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con".
 
 (* UNEXPORTED
-End More_Corollaries.
+End More_Corollaries
 *)
 
 (* UNEXPORTED
-Section More_Sums.
+Section More_Sums
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
+alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/f.var".
+alias id "f" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/f'.var".
+alias id "f'" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/derF.var".
+alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var".
 
 (* end show *)
 
@@ -361,11 +361,11 @@ inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con".
 
 (* UNEXPORTED
-End More_Sums.
+End More_Sums
 *)
 
 (* UNEXPORTED
-Section Diffble_Basic_Properties.
+Section Diffble_Basic_Properties
 *)
 
 (*#* **Differentiability
@@ -373,9 +373,9 @@ Section Diffble_Basic_Properties.
 Mutatis mutandis for differentiability.
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
+alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con".
 
@@ -383,13 +383,13 @@ inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G.var".
+alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
+alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/diffG.var".
+alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var".
 
 (*#*
 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
@@ -419,7 +419,7 @@ inline "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con".
 
 (* UNEXPORTED
-End Diffble_Basic_Properties.
+End Diffble_Basic_Properties
 *)
 
 (* UNEXPORTED
@@ -427,20 +427,20 @@ Hint Immediate Diffble_imp_inc: included.
 *)
 
 (* UNEXPORTED
-Section Diffble_Corollaries.
+Section Diffble_Corollaries
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
+alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/G.var".
+alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
+alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/diffG.var".
+alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con".
 
@@ -451,11 +451,11 @@ inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con".
 
 (* UNEXPORTED
-End Diffble_Corollaries.
+End Diffble_Corollaries
 *)
 
 (* UNEXPORTED
-Section Nth_Derivative.
+Section Nth_Derivative
 *)
 
 (*#* **Nth Derivative
@@ -463,12 +463,12 @@ Section Nth_Derivative.
 Higher order derivatives pose more interesting problems.  It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/pI.var".
+alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var".
 
 (* UNEXPORTED
-Section Definitions.
+Section Definitions
 *)
 
 (*#*
@@ -476,11 +476,11 @@ Section Definitions.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/n.var".
+alias id "n" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var".
 
-inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
+alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var".
 
 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con".
 
@@ -496,11 +496,11 @@ inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con".
 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con".
 
 (* UNEXPORTED
-End Definitions.
+End Definitions
 *)
 
 (* UNEXPORTED
-Section Basic_Results.
+Section Basic_Results
 *)
 
 (*#*
@@ -542,11 +542,11 @@ inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con".
 
 (* UNEXPORTED
-End Basic_Results.
+End Basic_Results
 *)
 
 (* UNEXPORTED
-Section More_Results.
+Section More_Results
 *)
 
 (*#*
@@ -570,22 +570,22 @@ inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con".
 
 (* UNEXPORTED
-End More_Results.
+End More_Results
 *)
 
 (* UNEXPORTED
-Section Derivating_Diffble.
+Section Derivating_Diffble
 *)
 
 (*#*
 As a special case we get a differentiation operator%\ldots%#...#
 *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/F.var".
+alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/MoreFunctions/diffF.var".
+alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var".
 
 (* end show *)
 
@@ -594,11 +594,11 @@ inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Deriv.con".
 
 (* UNEXPORTED
-End Derivating_Diffble.
+End Derivating_Diffble
 *)
 
 (* UNEXPORTED
-Section Corollaries.
+Section Corollaries
 *)
 
 (*#*
@@ -620,11 +620,11 @@ inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con".
 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con".
 
 (* UNEXPORTED
-End Corollaries.
+End Corollaries
 *)
 
 (* UNEXPORTED
-End Nth_Derivative.
+End Nth_Derivative
 *)
 
 (* UNEXPORTED