...

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/IntervalFunct.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/IntervalFunct.mma
index 03e744da801ec5b8470f01f013f29b6c80685ddf..cf4c9b991aeeb4e4d0c2d34b21349222d41e65b1 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/IntervalFunct.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/IntervalFunct.mma
@@ -45,21 +45,31 @@ type [I -> IR].
 %\end{convention}%
 *)
 
-alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Operations/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Operations/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Operations/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/Hab.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/Operations/I.con" "Operations__".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/Operations/I.con" "Operations__" as definition.
 
 (* end hide *)
 
-alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Operations/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/f.var
+*)
 
-alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Operations/g.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/g.var
+*)
 
 (* UNEXPORTED
 Section Const
@@ -72,39 +82,41 @@ Constant and identity functions are defined.
 %\end{convention}%
 *)
 
-alias id "c" = "cic:/CoRN/ftc/IntervalFunct/Operations/Const/c.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/Const/c.var
+*)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst.con" as definition.
 
 (* UNEXPORTED
 End Const
 *)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IId_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IId_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IId.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IId.con" as definition.
 
 (*#*
 Next, we define addition, algebraic inverse, subtraction and product of functions.
 *)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult.con" as definition.
 
 (* UNEXPORTED
 Section Nth_Power
@@ -114,11 +126,13 @@ Section Nth_Power
 Exponentiation to a natural power [n] is also useful.
 *)
 
-alias id "n" = "cic:/CoRN/ftc/IntervalFunct/Operations/Nth_Power/n.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/Nth_Power/n.var
+*)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/INth_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/INth_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/INth.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/INth.con" as definition.
 
 (* UNEXPORTED
 End Nth_Power
@@ -134,17 +148,19 @@ Section Recip_Div
 
 (* begin show *)
 
-alias id "Hg" = "cic:/CoRN/ftc/IntervalFunct/Operations/Recip_Div/Hg.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Operations/Recip_Div/Hg.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv.con" as definition.
 
 (* UNEXPORTED
 End Recip_Div
@@ -154,9 +170,9 @@ End Recip_Div
 Absolute value will also be needed at some point.
 *)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs.con" as definition.
 
 (* UNEXPORTED
 End Operations
@@ -184,39 +200,57 @@ compact interval [[a',b']], and let [g] be a setoid function of type
 Section Composition
 *)
 
-alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Composition/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Composition/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/Hab.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I.con" "Composition__".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I.con" "Composition__" as definition.
 
 (* end hide *)
 
-alias id "a'" = "cic:/CoRN/ftc/IntervalFunct/Composition/a'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/a'.var
+*)
 
-alias id "b'" = "cic:/CoRN/ftc/IntervalFunct/Composition/b'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/b'.var
+*)
 
-alias id "Hab'" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/Hab'.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I'.con" "Composition__".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I'.con" "Composition__" as definition.
 
 (* end hide *)
 
-alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Composition/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/f.var
+*)
 
-alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Composition/g.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/g.var
+*)
 
-alias id "Hfg" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hfg.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/IntervalFunct/Composition/Hfg.var
+*)
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp_strext.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp.con".
+inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp.con" as definition.
 
 (* UNEXPORTED
 End Composition