X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Funiform.ma;h=25cfe67cb6da3e02adbfd4283078c1f619708d21;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=41b593ae4a25832cc073a98c0702235f1c39be84;hpb=c3b8ed2e554cbdb677729747c5b5a96112ae5169;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index 41b593ae4..25cfe67cb 100644
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -29,23 +29,19 @@ definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 
 notation "a \subseteq u" left associative with precedence 70 
   for @{ 'subset $a $u }.
-interpretation "Bishop subset" 'subset a b =
-  (cic:/matita/dama/uniform/subset.con _ a b). 
+interpretation "Bishop subset" 'subset a b = (subset _ a b). 
 
 notation "hvbox({ ident x : t | break p })" non associative with precedence 50
   for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.  
 definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
-interpretation "explicit set" 'explicitset t =
-  (cic:/matita/dama/uniform/mk_set.con _ t).
+interpretation "explicit set" 'explicitset t = (mk_set _ t).
 
 notation < "s  2 \atop \neq" non associative with precedence 90
   for @{ 'square2 $s }.
 notation > "s 'square'" non associative with precedence 90
   for @{ 'square $s }.
-interpretation "bishop set square" 'square x =
-  (cic:/matita/dama/uniform/square_bishop_set.con x).    
-interpretation "bishop set square" 'square2 x =
-  (cic:/matita/dama/uniform/square_bishop_set.con x).    
+interpretation "bishop set square" 'square x = (square_bishop_set x).    
+interpretation "bishop set square" 'square2 x = (square_bishop_set x).    
 
 
 alias symbol "exists" = "exists".
@@ -56,12 +52,11 @@ definition compose_relations ≝
    
 notation "a \circ b"  left associative with precedence 60
   for @{'compose $a $b}.
-interpretation "relations composition" 'compose a b = 
- (cic:/matita/dama/uniform/compose_relations.con _ a b).
+interpretation "relations composition" 'compose a b = (compose_relations _ a b).
 notation "hvbox(x \in break a \circ break b)"  non associative with precedence 50
   for @{'compose2 $a $b $x}.
 interpretation "relations composition" 'compose2 a b x = 
- (cic:/matita/dama/uniform/compose_relations.con _ a b x).
+ (compose_relations _ a b x).
 
 definition invert_relation ≝
   λC:bishop_set.λU:C square → Prop.
@@ -73,10 +68,8 @@ notation < "s \sup (-1) x"  non associative with precedence 90
   for @{ 'invert2 $s $x}. 
 notation > "'inv' s" non associative with precedence 90
   for @{ 'invert $s }.
-interpretation "relation invertion" 'invert a = 
- (cic:/matita/dama/uniform/invert_relation.con _ a).
-interpretation "relation invertion" 'invert2 a x = 
- (cic:/matita/dama/uniform/invert_relation.con _ a x).
+interpretation "relation invertion" 'invert a = (invert_relation _ a).
+interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
 
 alias symbol "exists" = "CProp exists".
 alias symbol "and" (instance 18) = "constructive and".
@@ -103,8 +96,7 @@ notation < "a \nbsp 'is_cauchy'" non associative with precedence 50
   for @{'cauchy $a}.
 notation > "a 'is_cauchy'" non associative with precedence 50 
   for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s =
- (cic:/matita/dama/uniform/cauchy.con _ s).  
+interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).  
    
 (* Definition 2.15 *)  
 definition uniform_converge ≝
@@ -116,7 +108,7 @@ notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative
 notation > "a 'uniform_converges' x" non associative with precedence 50 
   for @{'uniform_converge $a $x}.
 interpretation "Uniform convergence" 'uniform_converge s u =
- (cic:/matita/dama/uniform/uniform_converge.con _ s u).
+ (uniform_converge _ s u).
  
 (* Lemma 2.16 *)
 lemma uniform_converge_is_cauchy : 
@@ -133,8 +125,7 @@ qed.
 (* Definition 2.17 *)
 definition mk_big_set ≝
   λP:CProp.λF:P→CProp.F.
-interpretation "explicit big set" 'explicitset t =
-  (cic:/matita/dama/uniform/mk_big_set.con _ t).
+interpretation "explicit big set" 'explicitset t = (mk_big_set _ t).
     
 definition restrict_uniformity ≝
   λC:uniform_space.λX:C→Prop.