X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fbasic_topologies_to_o-basic_topologies.ma;h=6b07dfeb0863a9c493d9b71d90bb42361054de7d;hb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;hp=0aeb58c737a459c5b691a21561a37ba199cfa610;hpb=bc477154d15f6979c948f9af602199af547d193e;p=helm.git

diff --git a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
index 0aeb58c73..6b07dfeb0 100644
--- a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
@@ -15,7 +15,7 @@
 include "formal_topology/basic_topologies.ma".
 include "formal_topology/o-basic_topologies.ma".
 include "formal_topology/relations_to_o-algebra.ma".
-
+(*
 definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology.
  intros (b); constructor 1;
   [ apply (POW' b) | apply (A b) | apply (J b);
@@ -29,7 +29,7 @@ definition o_continuous_relation_of_continuous_relation:
   [ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ]
 qed.
 
-axiom daemon: ⊥. (*FG: alla faccia del costruttivismo *)
+axiom daemon: False.
 
 lemma o_continuous_relation_of_continuous_relation_morphism :
   ∀S,T:category2_of_category1 BTop.
@@ -89,3 +89,4 @@ theorem BTop_to_OBTop_full: full2 ?? BTop_to_OBTop.
    unfold image_coercion; cases Hg; whd; simplify; intro; simplify;
 qed.
 *)
+