X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Funiform.ma;h=d6637a85db89416896072733424d9c95bfa2c328;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=759037124310076d813c711ea272eb323d2d6ffc;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git

diff --git a/helm/software/matita/library/dama/uniform.ma b/helm/software/matita/library/dama/uniform.ma
index 759037124..d6637a85d 100644
--- a/helm/software/matita/library/dama/uniform.ma
+++ b/helm/software/matita/library/dama/uniform.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "supremum.ma".
+include "dama/supremum.ma".
 
 (* Definition 2.13 *)
 alias symbol "pair" = "Pair construction".
@@ -26,17 +26,17 @@ definition compose_os_relations ≝
   λC:ordered_set.λU,V:C squareB → Prop.
    λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
    
-interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
-interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
+interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations ? a b).
+interpretation "ordered set relations composition" 'compose a b = (compose_os_relations ? a b).
 
 definition invert_bs_relation ≝
   λC:bishop_set.λU:C squareB → Prop.
     λx:C squareB. U 〈\snd x,\fst x〉.
       
 notation > "\inv" with precedence 60 for @{ 'invert_symbol  }.
-interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
+interpretation "relation invertion" 'invert a = (invert_bs_relation ? a).
+interpretation "relation invertion" 'invert_symbol = (invert_bs_relation ?).
+interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation ? a x).
 
 alias symbol "exists" = "CProp exists".
 alias symbol "compose" = "bishop set relations composition".
@@ -65,7 +65,7 @@ notation < "a \nbsp 'is_cauchy'" non associative with precedence 45
   for @{'cauchy $a}.
 notation > "a 'is_cauchy'" non associative with precedence 45 
   for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).  
+interpretation "Cauchy sequence" 'cauchy s = (cauchy ? s).  
    
 (* Definition 2.15 *)  
 definition uniform_converge ≝
@@ -77,7 +77,7 @@ notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative
 notation > "a 'uniform_converges' x" non associative with precedence 45 
   for @{'uniform_converge $a $x}.
 interpretation "Uniform convergence" 'uniform_converge s u =
- (uniform_converge _ s u).
+ (uniform_converge ? s u).
  
 (* Lemma 2.16 *)
 lemma uniform_converge_is_cauchy :