From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 29 Jan 2009 11:48:31 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4222
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d4cd2564126b15d4f0aa736353d25dfc34d2cad8;hp=887916a4791bba656b1dec730d3315239d3c1f21;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
index 6b6469f27..ee9682cec 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
@@ -19,7 +19,7 @@ include "relations_to_o-algebra.ma".
 definition o_basic_topology_of_basic_topology: cic:/matita/formal_topology/basic_topologies/basic_topology.ind#xpointer(1/1) → basic_topology.
  intro;
  constructor 1;
-  [ apply (SUBSETS b);
+  [ apply (POW' b);
   | apply (A b);
   | apply (J b);
   | apply (A_is_saturation b);
diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
index 97bfcd6c9..88a18fda7 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
@@ -19,7 +19,7 @@ include "relations_to_o-algebra.ma".
 (* These are only conversions :-) *)
 
 definition o_operator_of_operator:
- ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C).
+ ∀C:REL. (Ω \sup C => Ω \sup C) → (POW C ⇒ POW C).
  intros (C t);apply t;
 qed.