X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fformal_topologies.ma;h=24dfb772186f8bc733b421cd98f03fb66ce67492;hb=1470ff47df1349333c6b721a1c162cc7dfc6806f;hp=a611e22ea9d5620404f2045e597824001ab1b80a;hpb=cb98bd7054893edee16aadd6741ec5210b04afbc;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
index a611e22ea..24dfb7721 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
@@ -14,7 +14,7 @@
 
 include "basic_topologies.ma".
 
-
+(*
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
   [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
@@ -24,7 +24,7 @@ definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
     try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
 qed.
 
-interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
+interpretation "downarrow" 'downarrow a = (fun_1 ?? (downarrow ?) a).
 
 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
@@ -32,7 +32,7 @@ definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω
   | intros; apply (.= (†H)‡(†H1)); apply refl1]
 qed.
 
-interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+interpretation "ffintersects" 'fintersects U V = (fun1 ??? (ffintersects ?) U V).
 
 record formal_topology: Type ≝
  { bt:> BTop;
@@ -46,7 +46,7 @@ definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
   | intros; apply (.= (†H)‡(†H1)); apply refl1]
 qed.
 
-interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
+interpretation "ffintersects'" 'fintersects U V = (fun1 ??? (ffintersects' ?) U V).
 
 record formal_map (S,T: formal_topology) : Type ≝
  { cr:> continuous_relation_setoid S T;
@@ -94,3 +94,4 @@ definition formal_map_composition:
     apply prop1; assumption]
 qed.
 
+*)
\ No newline at end of file