From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 26 Sep 2008 08:43:35 +0000 (+0000)
Subject: commented out a line that was making the file fail
X-Git-Tag: make_still_working~4733
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a29aa43eb607d019699f0a76dc83e7093e5b222;p=helm.git

commented out a line that was making the file fail
---

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 41c0d5c53..190e00e5d 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -172,8 +172,9 @@ definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 
 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 
+(*
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;
-   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
  }.
-
+*)