X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fclassical_pointwise%2Fsets.ma;h=6033f4db21aac0dc8992c0f98bbe47399eb5c16f;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=48f07c2d6ccbbacae98dc074787f594e7a40577f;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma b/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma
index 48f07c2d6..6033f4db2 100644
--- a/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma
+++ b/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma
@@ -22,12 +22,12 @@ definition set   ≝   λX:Type.X → Prop.
 
 definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x.
 
-notation "hvbox(x break ∈ A)" with precedence 60
+notation "hvbox(x break ∈ A)" with precedence 65
 for @{ 'member_of $x $A }.
 
 interpretation "Member of" 'member_of x A = (mk_member_of ? A x).
  
-notation "hvbox(x break ∉ A)" with precedence 60
+notation "hvbox(x break ∉ A)" with precedence 65
 for @{ 'not_member_of $x $A }.
 
 interpretation "Not member of" 'not_member_of x A = (Not (member_of ? A x)).
@@ -40,7 +40,7 @@ interpretation "Emptyset" 'emptyset = (emptyset ?).
 
 definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
 
-notation "hvbox(A break ⊆ B)" with precedence 60
+notation "hvbox(A break ⊆ B)" with precedence 65
 for @{ 'subset $A $B }.
 
 interpretation "Subset" 'subset A B = (subset ? A B).
@@ -55,7 +55,7 @@ interpretation "Intersection" 'intersection A B = (intersection ? A B).
  
 definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
 
-notation "hvbox(A break ∪ B)" with precedence 65
+notation "hvbox(A break ∪ B)" with precedence 66
 for @{ 'union $A $B }.
 
 interpretation "Union" 'union A B = (union ? A B).
@@ -72,7 +72,7 @@ interpretation "nth" 'nth A i = (nth ? A i).
 definition countable_union: ∀X. seq (set X) → set X ≝ 
  λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
 
-notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
+notation "∪ \sub (ident i opt (: ty)) B" with precedence 66
 for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
 
 interpretation "countable_union" 'big_union η.t = (countable_union ? t).