X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fsubsets.ma;h=56c2c895cbb98d2495b099e88c919792481075d2;hb=7c9d99dfb049d726491b71f07ba6a9b088b30166;hp=15bfb98d3b395b78e4c80c78514a0b63de252e2a;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

diff --git a/matita/matita/lib/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma
index 15bfb98d3..56c2c895c 100644
--- 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 }.
@@ -164,18 +166,19 @@ definition big_union: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
 qed.
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (\emsp) term 90 p)" 
-non associative with precedence 50 for @{ 'bigcup $p }.
+non associative with precedence 55 for @{ 'bigcup $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
-notation > "hovbox(⋃ f)" non associative with precedence 60 for @{ 'bigcup $f }.
+non associative with precedence 55 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋃ f)" non associative with precedence 65 for @{ 'bigcup $f }.
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (\emsp) term 90 p)" 
-non associative with precedence 50 for @{ 'bigcap $p }.
+non associative with precedence 55 for @{ 'bigcap $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }.
-notation > "hovbox(⋂ f)" non associative with precedence 60 for @{ 'bigcap $f }.
+non associative with precedence 55 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋂ f)" non associative with precedence 65 for @{ 'bigcap $f }.
 
 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 ?)).
+*)