X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_uniform.ma;h=3bdfbe978f37a837f6aed589d7c46cac56aee8c5;hb=c3b8ed2e554cbdb677729747c5b5a96112ae5169;hp=63f263d274296119010fd9aee822fce2fab8fce9;hpb=28bcf58da6b3726320b368ce4d1d8e2356b4df1b;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 63f263d27..3bdfbe978 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -153,4 +153,3 @@ qed.
 definition order_continuity ≝
   λC:ordered_uniform_space.∀a:sequence C.∀x:C.
     (a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).
-