X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdatatypes%2Fsubsets.ma;h=8e2eda4c99508749053bc3041154e814cdf27fd6;hb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;hp=7c9a13195f2ba6f07635f3067c5e4e942a07d095;hpb=c96d1f2066d37b84a34412f7c49fb3e4f54bd9a2;p=helm.git

diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma
index 7c9a13195..8e2eda4c9 100644
--- a/helm/software/matita/library/datatypes/subsets.ma
+++ b/helm/software/matita/library/datatypes/subsets.ma
@@ -26,6 +26,8 @@ theorem transitive_subseteq_operator: ∀A. transitive ? (subseteq_operator A).
  assumption.
 qed.
 
+(*
+
 definition powerset_setoid: setoid → setoid1.
  intros (T);
  constructor 1;
@@ -57,7 +59,7 @@ definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
      | apply s1; assumption]]
 qed.     
 
-interpretation "mem" 'mem a S = (fun1 ___ (mem _) a S).
+interpretation "mem" 'mem a S = (fun1 ??? (mem ?) a S).
 
 definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
  intros;
@@ -72,7 +74,7 @@ definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
       apply (transitive_subseteq_operator ???? s s4) ]]
 qed.
 
-interpretation "subseteq" 'subseteq U V = (fun1 ___ (subseteq _) U V).
+interpretation "subseteq" 'subseteq U V = (fun1 ??? (subseteq ?) U V).
 
 theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
  intros 4; assumption.
@@ -94,7 +96,7 @@ definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
      | apply (. #‡(H1 \sup -1)); assumption]]
 qed.
 
-interpretation "overlaps" 'overlaps U V = (fun1 ___ (overlaps _) U V).
+interpretation "overlaps" 'overlaps U V = (fun1 ??? (overlaps ?) U V).
 
 definition intersects:
  ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
@@ -108,7 +110,7 @@ definition intersects:
     | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
 qed.
 
-interpretation "intersects" 'intersects U V = (fun1 ___ (intersects _) U V).
+interpretation "intersects" 'intersects U V = (fun1 ??? (intersects ?) U V).
 
 definition union:
  ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
@@ -122,7 +124,7 @@ definition union:
     | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
 qed.
 
-interpretation "union" 'union U V = (fun1 ___ (union _) U V).
+interpretation "union" 'union U V = (fun1 ??? (union ?) U V).
 
 definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
  intros; constructor 1;
@@ -135,4 +137,6 @@ definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
      [ apply a |4: apply a'] try assumption; apply sym; assumption]
 qed.
 
-interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a).
+interpretation "singleton" 'singl a = (fun_1 ?? (singleton ?) a).
+
+*)
\ No newline at end of file