X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FWeakIVT.ma;h=e22afe085688b11ea956ed33d50ef2d242a7fbac;hb=2951babfd31047ac057714130157da2bc36e906e;hp=8001b5376630bb5c156f1a407c3d0dcc85f69eb7;hpb=52206fa1c090fcdc8386ec8d7e88beca089c7e39;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma b/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma
index 8001b5376..e22afe085 100644
--- a/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma
+++ b/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma
@@ -44,24 +44,24 @@ will prove them here.
 *)
 
 (* UNEXPORTED
-Section Lemma1.
+Section Lemma1
 *)
 
-inline "cic:/CoRN/ftc/WeakIVT/a.var".
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma1/a.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/b.var".
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma1/b.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma1/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/I.con".
+inline "cic:/CoRN/ftc/WeakIVT/Lemma1/I.con" "Lemma1__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/F.var".
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma1/F.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma1/contF.var".
 
 (*#* **First Lemmas
 
@@ -77,28 +77,28 @@ enough to [z].
 inline "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_lft.con".
 
 (* UNEXPORTED
-End Lemma1.
+End Lemma1
 *)
 
 (* UNEXPORTED
-Section Lemma2.
+Section Lemma2
 *)
 
-inline "cic:/CoRN/ftc/WeakIVT/a.var".
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma2/a.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/b.var".
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma2/b.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma2/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/I.con".
+inline "cic:/CoRN/ftc/WeakIVT/Lemma2/I.con" "Lemma2__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/F.var".
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma2/F.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma2/contF.var".
 
 (*#*
 If [f(b) [<] f(a)], a similar result holds:
@@ -107,11 +107,11 @@ If [f(b) [<] f(a)], a similar result holds:
 inline "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_rht.con".
 
 (* UNEXPORTED
-End Lemma2.
+End Lemma2
 *)
 
 (* UNEXPORTED
-Section IVT.
+Section IVT
 *)
 
 (*#* **The IVT
@@ -122,53 +122,53 @@ these assumptions, we can build two sequences of values which
 converge to [x0] such that [f(x0) [=] z].
 *)
 
-inline "cic:/CoRN/ftc/WeakIVT/a.var".
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/IVT/a.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/b.var".
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/IVT/b.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/Hab'.var".
+alias id "Hab'" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab'.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/I.con".
+inline "cic:/CoRN/ftc/WeakIVT/IVT/I.con" "IVT__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/F.var".
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/IVT/F.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/IVT/contF.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/incF.con".
+inline "cic:/CoRN/ftc/WeakIVT/IVT/incF.con" "IVT__".
 
 (* end hide *)
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/WeakIVT/incrF.var".
+alias id "incrF" = "cic:/CoRN/ftc/WeakIVT/IVT/incrF.var".
 
 (* end show *)
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/WeakIVT/Ha.con".
+inline "cic:/CoRN/ftc/WeakIVT/IVT/Ha.con" "IVT__".
 
-inline "cic:/CoRN/ftc/WeakIVT/Hb.con".
+inline "cic:/CoRN/ftc/WeakIVT/IVT/Hb.con" "IVT__".
 
-inline "cic:/CoRN/ftc/WeakIVT/HFab'.con".
+inline "cic:/CoRN/ftc/WeakIVT/IVT/HFab'.con" "IVT__".
 
 (* end hide *)
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/WeakIVT/z.var".
+alias id "z" = "cic:/CoRN/ftc/WeakIVT/IVT/z.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/Haz.var".
+alias id "Haz" = "cic:/CoRN/ftc/WeakIVT/IVT/Haz.var".
 
-inline "cic:/CoRN/ftc/WeakIVT/Hzb.var".
+alias id "Hzb" = "cic:/CoRN/ftc/WeakIVT/IVT/Hzb.var".
 
 (* end show *)
 
@@ -221,9 +221,9 @@ inline "cic:/CoRN/ftc/WeakIVT/a_seq_Cauchy.con".
 
 inline "cic:/CoRN/ftc/WeakIVT/b_seq_Cauchy.con".
 
-inline "cic:/CoRN/ftc/WeakIVT/xa.con".
+inline "cic:/CoRN/ftc/WeakIVT/IVT/xa.con" "IVT__".
 
-inline "cic:/CoRN/ftc/WeakIVT/xb.con".
+inline "cic:/CoRN/ftc/WeakIVT/IVT/xb.con" "IVT__".
 
 inline "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_lim.con".
 
@@ -232,6 +232,6 @@ inline "cic:/CoRN/ftc/WeakIVT/xa_in_interval.con".
 inline "cic:/CoRN/ftc/WeakIVT/IVT_I.con".
 
 (* UNEXPORTED
-End IVT.
+End IVT
 *)