X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fo-basic_topologies.ma;h=095c43805619695526d55380a17f5683633b5cdb;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=0e9d8604f00c5d10cdf1037fcb3faac287b2775e;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

diff --git a/matita/matita/lib/formal_topology/o-basic_topologies.ma b/matita/matita/lib/formal_topology/o-basic_topologies.ma
index 0e9d8604f..095c43805 100644
--- a/matita/matita/lib/formal_topology/o-basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/o-basic_topologies.ma
@@ -14,7 +14,7 @@
 
 include "formal_topology/o-algebra.ma".
 include "formal_topology/o-saturations.ma".
-
+(*
 record Obasic_topology: Type[2] ≝ { 
    Ocarrbt:> OA;
    oA: Ocarrbt ⇒_2 Ocarrbt; oJ: Ocarrbt ⇒_2 Ocarrbt;
@@ -188,3 +188,4 @@ theorem continuous_relation_eqS:
  apply Hcut2; assumption.
 qed.
 *)
+*)