X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fsaturations_to_o-saturations.ma;h=ebea817d077d453374fa97c1c0c8569687d15010;hb=3c257bf84769adf162510ed86a89872e3003629a;hp=39b4176cb419aecbf558f50fc6b5f70e27e5f0b9;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

diff --git a/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma b/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma
index 39b4176cb..ebea817d0 100644
--- a/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma
+++ b/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma
@@ -15,7 +15,7 @@
 include "formal_topology/saturations.ma".
 include "formal_topology/o-saturations.ma".
 include "formal_topology/relations_to_o-algebra.ma".
-
+(*
 (* These are only conversions :-) *)
 
 definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)) ≝ λC,t.t.
@@ -27,3 +27,4 @@ intros (C R i); apply i; qed.
 definition is_o_reduction_of_is_reduction: 
   ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
 intros (C R i); apply i; qed.
+*)