X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdatatypes%2Fsubsets.ma;h=8c7963d67ea3a28b3073cadb844f27d1d25f713a;hb=0137a346eaaf9ae7a0b23c7a3b4c6628073b7dfb;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..8c7963d67 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;
@@ -136,3 +138,5 @@ definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
 qed.
 
 interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a).
+
+*)
\ No newline at end of file