decentralizing core notation

[helm.git] / matita / matita / lib / formal_topology / subsets.ma

diff --git a/matita/matita/lib/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma
index 8bacd2a5538ce15df4168e0e9675a69d69dd69c0..56c2c895cbb98d2495b099e88c919792481075d2 100644 (file)
--- a/matita/matita/lib/formal_topology/subsets.ma
+++ b/matita/matita/lib/formal_topology/subsets.ma
@@ -13,7 +13,9 @@
 (**************************************************************************)
 
 include "formal_topology/categories.ma".
-
+include "basics/core_notation/singl_1.ma".
+include "basics/core_notation/subset_1.ma".
+(*
 record powerset_carrier (A: objs1 SET) : Type[1] ≝ { mem_operator: A ⇒_1 CPROP }.
 interpretation "powerset low" 'powerset A = (powerset_carrier A).
 notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
@@ -179,3 +181,4 @@ interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f).
 interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f).
 interpretation "bigcup mk" 'bigcup_mk f = (fun12 ?? (big_union ??) (mk_unary_morphism2 ?? f ?)).
 interpretation "bigcap mk" 'bigcap_mk f = (fun12 ?? (big_intersects ??) (mk_unary_morphism2 ?? f ?)).
+*)