X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FPartInterval.ma;h=a46add4bca731c3ee69e946037d162a062528fe4;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=3013ac376b0afe98f3126a80330bbc66aaa98b46;hpb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/ftc/PartInterval.ma b/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
index 3013ac376..a46add4bc 100644
--- a/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
+++ b/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
@@ -16,14 +16,14 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartInterval".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
 
 include "ftc/IntervalFunct.ma".
 
 (* UNEXPORTED
-Section Conversion.
+Section Conversion
 *)
 
 (*#* *Correspondence
@@ -45,28 +45,28 @@ that [I [=] [a,b]] is included in the domain of [F].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/PartInterval/F.var".
+alias id "F" = "cic:/CoRN/ftc/PartInterval/Conversion/F.var".
 
-inline "cic:/CoRN/ftc/PartInterval/a.var".
+alias id "a" = "cic:/CoRN/ftc/PartInterval/Conversion/a.var".
 
-inline "cic:/CoRN/ftc/PartInterval/b.var".
+alias id "b" = "cic:/CoRN/ftc/PartInterval/Conversion/b.var".
 
-inline "cic:/CoRN/ftc/PartInterval/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Conversion/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/PartInterval/I.con".
+inline "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/PartInterval/Hf.var".
+alias id "Hf" = "cic:/CoRN/ftc/PartInterval/Conversion/Hf.var".
 
 inline "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con".
 
 inline "cic:/CoRN/ftc/PartInterval/IntPartIR.con".
 
 (* UNEXPORTED
-End Conversion.
+End Conversion
 *)
 
 (* UNEXPORTED
@@ -74,7 +74,7 @@ Implicit Arguments IntPartIR [F a b Hab].
 *)
 
 (* UNEXPORTED
-Section AntiConversion.
+Section AntiConversion
 *)
 
 (*#*
@@ -82,26 +82,26 @@ To go the other way around, we simply take a setoid function [f] with
 domain [[a,b]] and build the corresponding partial function.
 *)
 
-inline "cic:/CoRN/ftc/PartInterval/a.var".
+alias id "a" = "cic:/CoRN/ftc/PartInterval/AntiConversion/a.var".
 
-inline "cic:/CoRN/ftc/PartInterval/b.var".
+alias id "b" = "cic:/CoRN/ftc/PartInterval/AntiConversion/b.var".
 
-inline "cic:/CoRN/ftc/PartInterval/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/AntiConversion/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/PartInterval/I.con".
+inline "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/PartInterval/f.var".
+alias id "f" = "cic:/CoRN/ftc/PartInterval/AntiConversion/f.var".
 
 inline "cic:/CoRN/ftc/PartInterval/PartInt_strext.con".
 
 inline "cic:/CoRN/ftc/PartInterval/PartInt.con".
 
 (* UNEXPORTED
-End AntiConversion.
+End AntiConversion
 *)
 
 (* UNEXPORTED
@@ -109,7 +109,7 @@ Implicit Arguments PartInt [a b Hab].
 *)
 
 (* UNEXPORTED
-Section Inverses.
+Section Inverses
 *)
 
 (*#*
@@ -119,11 +119,11 @@ In one direction these operators are inverses.
 inline "cic:/CoRN/ftc/PartInterval/int_part_int.con".
 
 (* UNEXPORTED
-End Inverses.
+End Inverses
 *)
 
 (* UNEXPORTED
-Section Equivalences.
+Section Equivalences
 *)
 
 (*#* **Mappings Preserve Operations
@@ -137,31 +137,31 @@ type [I->IR] equal respectively to [F] and [G] in [I].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/PartInterval/F.var".
+alias id "F" = "cic:/CoRN/ftc/PartInterval/Equivalences/F.var".
 
-inline "cic:/CoRN/ftc/PartInterval/G.var".
+alias id "G" = "cic:/CoRN/ftc/PartInterval/Equivalences/G.var".
 
-inline "cic:/CoRN/ftc/PartInterval/a.var".
+alias id "a" = "cic:/CoRN/ftc/PartInterval/Equivalences/a.var".
 
-inline "cic:/CoRN/ftc/PartInterval/b.var".
+alias id "b" = "cic:/CoRN/ftc/PartInterval/Equivalences/b.var".
 
-inline "cic:/CoRN/ftc/PartInterval/c.var".
+alias id "c" = "cic:/CoRN/ftc/PartInterval/Equivalences/c.var".
 
-inline "cic:/CoRN/ftc/PartInterval/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/PartInterval/I.con".
+inline "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/PartInterval/f.var".
+alias id "f" = "cic:/CoRN/ftc/PartInterval/Equivalences/f.var".
 
-inline "cic:/CoRN/ftc/PartInterval/g.var".
+alias id "g" = "cic:/CoRN/ftc/PartInterval/Equivalences/g.var".
 
-inline "cic:/CoRN/ftc/PartInterval/Ff.var".
+alias id "Ff" = "cic:/CoRN/ftc/PartInterval/Equivalences/Ff.var".
 
-inline "cic:/CoRN/ftc/PartInterval/Gg.var".
+alias id "Gg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var".
 
 inline "cic:/CoRN/ftc/PartInterval/part_int_const.con".
 
@@ -179,9 +179,9 @@ inline "cic:/CoRN/ftc/PartInterval/part_int_nth.con".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/PartInterval/HG.var".
+alias id "HG" = "cic:/CoRN/ftc/PartInterval/Equivalences/HG.var".
 
-inline "cic:/CoRN/ftc/PartInterval/Hg.var".
+alias id "Hg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hg.var".
 
 (* end show *)
 
@@ -190,6 +190,6 @@ inline "cic:/CoRN/ftc/PartInterval/part_int_recip.con".
 inline "cic:/CoRN/ftc/PartInterval/part_int_div.con".
 
 (* UNEXPORTED
-End Equivalences.
+End Equivalences
 *)