minor changes to make the library compile after wilmers new exists.

[helm.git] / helm / software / matita / library / dama / models / nat_lebesgue.ma

diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma
index 8d563b1e351d469c4cb2097dda9fcd094b689915..2657aba89dd37f3f76645fdd7fcc81f0aafbe0bf 100644 (file)
--- a/helm/software/matita/library/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma
@@ -15,6 +15,7 @@
 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 →