X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fclassical_pointwise%2Fsets.ma;h=5b8bdd7bdd5c868b542c8a7d85c75f1156d7bc44;hb=be527f5bd4acaf530d8843b23e6849fd5211e1fc;hp=f03c3e7f21d87e85952614efb8d8b6f35c14a6d4;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma b/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma
index f03c3e7f2..5b8bdd7bd 100644
--- a/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma
@@ -25,30 +25,25 @@ definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x.
 notation "hvbox(x break ∈ A)" with precedence 60
 for @{ 'member_of $x $A }.
 
-interpretation "Member of" 'member_of x A =
- (cic:/matita/classical_pointwise/sets/member_of.con _ A x).
+interpretation "Member of" 'member_of x A = (mk_member_of _ A x).
  
 notation "hvbox(x break ∉ A)" with precedence 60
 for @{ 'not_member_of $x $A }.
 
-interpretation "Not member of" 'not_member_of x A =
- (cic:/matita/logic/connectives/Not.con
-  (cic:/matita/classical_pointwise/sets/member_of.con _ A x)).
+interpretation "Not member of" 'not_member_of x A = (Not (member_of _ A x)).
 
 definition emptyset : ∀X.set X ≝  λX:Type.λx:X.False.
 
 notation "∅︀" with precedence 100 for @{ 'emptyset }.
 
-interpretation "Emptyset" 'emptyset =
- (cic:/matita/classical_pointwise/sets/emptyset.con _).
+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
 for @{ 'subset $A $B }.
 
-interpretation "Subset" 'subset A B =
- (cic:/matita/classical_pointwise/sets/subset.con _ A B).
+interpretation "Subset" 'subset A B = (subset _ A B).
  
 definition intersection: ∀X. set X → set X → set X ≝ 
  λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
@@ -56,16 +51,14 @@ definition intersection: ∀X. set X → set X → set X ≝
 notation "hvbox(A break ∩ B)" with precedence 70
 for @{ 'intersection $A $B }.
 
-interpretation "Intersection" 'intersection A B =
- (cic:/matita/classical_pointwise/sets/intersection.con _ A B).
+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
 for @{ 'union $A $B }.
 
-interpretation "Union" 'union A B =
- (cic:/matita/classical_pointwise/sets/union.con _ A B).
+interpretation "Union" 'union A B = (union _ A B).
 
 definition seq ≝ λX:Type.nat → X.
 
@@ -74,8 +67,7 @@ definition nth ≝  λX.λA:seq X.λi.A i.
 notation "hvbox(A \sub i)" with precedence 100
 for @{ 'nth $A $i }.
 
-interpretation "nth" 'nth A i =
- (cic:/matita/classical_pointwise/sets/nth.con _ A i).
+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.
@@ -83,16 +75,14 @@ definition countable_union: ∀X. seq (set X) → set X ≝
 notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
 for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
 
-interpretation "countable_union" 'big_union η.t =
- (cic:/matita/classical_pointwise/sets/countable_union.con _ t).  
+interpretation "countable_union" 'big_union η.t = (countable_union _ t).  
 
 definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
 
 notation "A \sup 'c'" with precedence 100
 for @{ 'complement $A }.
 
-interpretation "Complement" 'complement A =
- (cic:/matita/classical_pointwise/sets/complement.con _ A).
+interpretation "Complement" 'complement A = (complement _ A).
  
 definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
  λX,Y,f,B,x. f x ∈ B.
@@ -100,5 +90,4 @@ definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
 notation "hvbox(f \sup (-1))" with precedence 100
 for @{ 'finverse $f }.
 
-interpretation "Inverse image" 'finverse f =
- (cic:/matita/classical_pointwise/sets/inverse_image.con _ _ f).
+interpretation "Inverse image" 'finverse f = (inverse_image _ _ f).