X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FIntervalFunct.ma;h=b08ef762b7c05f49f29118afddf1d91298a2469f;hb=55e5bef77f163b29feeb9ad4e83376c5aa301297;hp=f2af4cc82375d42ce989d813d0604d8585bbfb4a;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma
index f2af4cc82..b08ef762b 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma
@@ -16,14 +16,14 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/IntervalFunct".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: IntervalFunct.v,v 1.5 2004/04/08 15:28:06 lcf Exp $ *)
 
 include "ftc/PartFunEquality.ma".
 
 (* UNEXPORTED
-Section Operations.
+Section Operations
 *)
 
 (*#* * Functions with compact domain
@@ -47,24 +47,24 @@ type [I -> IR].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/a.var".
+alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Operations/a.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/b.var".
+alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Operations/b.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Operations/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/I.con".
+inline "cic:/CoRN/ftc/IntervalFunct/Operations/I.con" "Operations__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/f.var".
+alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Operations/f.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/g.var".
+alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Operations/g.var".
 
 (* UNEXPORTED
-Section Const.
+Section Const
 *)
 
 (*#*
@@ -74,14 +74,14 @@ Constant and identity functions are defined.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/c.var".
+alias id "c" = "cic:/CoRN/ftc/IntervalFunct/Operations/Const/c.var".
 
 inline "cic:/CoRN/ftc/IntervalFunct/IConst_strext.con".
 
 inline "cic:/CoRN/ftc/IntervalFunct/IConst.con".
 
 (* UNEXPORTED
-End Const.
+End Const
 *)
 
 inline "cic:/CoRN/ftc/IntervalFunct/IId_strext.con".
@@ -109,21 +109,21 @@ inline "cic:/CoRN/ftc/IntervalFunct/IMult_strext.con".
 inline "cic:/CoRN/ftc/IntervalFunct/IMult.con".
 
 (* UNEXPORTED
-Section Nth_Power.
+Section Nth_Power
 *)
 
 (*#*
 Exponentiation to a natural power [n] is also useful.
 *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/n.var".
+alias id "n" = "cic:/CoRN/ftc/IntervalFunct/Operations/Nth_Power/n.var".
 
 inline "cic:/CoRN/ftc/IntervalFunct/INth_strext.con".
 
 inline "cic:/CoRN/ftc/IntervalFunct/INth.con".
 
 (* UNEXPORTED
-End Nth_Power.
+End Nth_Power
 *)
 
 (*#*
@@ -131,12 +131,12 @@ If a function is non-zero in all the interval then we can define its multiplicat
 *)
 
 (* UNEXPORTED
-Section Recip_Div.
+Section Recip_Div
 *)
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/Hg.var".
+alias id "Hg" = "cic:/CoRN/ftc/IntervalFunct/Operations/Recip_Div/Hg.var".
 
 (* end show *)
 
@@ -149,7 +149,7 @@ inline "cic:/CoRN/ftc/IntervalFunct/IDiv_strext.con".
 inline "cic:/CoRN/ftc/IntervalFunct/IDiv.con".
 
 (* UNEXPORTED
-End Recip_Div.
+End Recip_Div
 *)
 
 (*#*
@@ -161,7 +161,7 @@ inline "cic:/CoRN/ftc/IntervalFunct/IAbs_strext.con".
 inline "cic:/CoRN/ftc/IntervalFunct/IAbs.con".
 
 (* UNEXPORTED
-End Operations.
+End Operations
 *)
 
 (*#* 
@@ -183,45 +183,45 @@ compact interval [[a',b']], and let [g] be a setoid function of type
 *)
 
 (* UNEXPORTED
-Section Composition.
+Section Composition
 *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/a.var".
+alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Composition/a.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/b.var".
+alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Composition/b.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/I.con".
+inline "cic:/CoRN/ftc/IntervalFunct/Composition/I.con" "Composition__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/a'.var".
+alias id "a'" = "cic:/CoRN/ftc/IntervalFunct/Composition/a'.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/b'.var".
+alias id "b'" = "cic:/CoRN/ftc/IntervalFunct/Composition/b'.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/Hab'.var".
+alias id "Hab'" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab'.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/I'.con".
+inline "cic:/CoRN/ftc/IntervalFunct/Composition/I'.con" "Composition__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/IntervalFunct/f.var".
+alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Composition/f.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/g.var".
+alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Composition/g.var".
 
-inline "cic:/CoRN/ftc/IntervalFunct/Hfg.var".
+alias id "Hfg" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hfg.var".
 
 inline "cic:/CoRN/ftc/IntervalFunct/IComp_strext.con".
 
 inline "cic:/CoRN/ftc/IntervalFunct/IComp.con".
 
 (* UNEXPORTED
-End Composition.
+End Composition
 *)
 
 (* UNEXPORTED