X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fmodels%2Fnat_lebesgue.ma;h=2657aba89dd37f3f76645fdd7fcc81f0aafbe0bf;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=d5e65215ec43a4bdaa3bc18be7d10acad54555c5;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git

diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma
index d5e65215e..2657aba89 100644
--- a/helm/software/matita/library/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lebesgue.ma".
-include "models/nat_order_continuous.ma".
+include "dama/lebesgue.ma".
+include "dama/models/nat_order_continuous.ma".
 
+alias symbol "dependent_pair" = "dependent pair".
 theorem nat_lebesgue_oc:
    ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s. 
      ∀x:ℕ.a order_converges x →