commented out a line that was making the file fail

[helm.git] / helm / software / matita / library / demo / formal_topology.ma

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 41c0d5c53cb2253fe4a9ea2e0deca0c275d89529..190e00e5d0eb549e6822d06c0e72fc6d9efe18a4 100644 (file)
--- 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)
  }.
-
+*)