...

[helm.git] / helm / software / matita / contribs / dama / dama / supremum.ma

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index a492c8f3299e8255c0b86be2605972da857b3310..6fa8e35ad86df21bcad372561711315560c0ed52 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -93,15 +93,15 @@ definition strictly_increasing ≝
 definition strictly_decreasing ≝ 
   λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n).
 
-notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45 
   for @{'strictly_increasing $s}.
-notation > "s 'is_strictly_increasing'" non associative with precedence 50 
+notation > "s 'is_strictly_increasing'" non associative with precedence 45 
   for @{'strictly_increasing $s}.
 interpretation "Ordered set strict increasing"  'strictly_increasing s    = 
   (strictly_increasing _ s).
-notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
-notation > "s 'is_strictly_decreasing'" non associative with precedence 50 
+notation > "s 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    = 
   (strictly_decreasing _ s).
@@ -227,13 +227,12 @@ notation > "a 'order_converges' x" non associative with precedence 45
 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).   
     
 (* Definition 2.8 *)
-alias symbol "and" = "constructive and".
 definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
 
-notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
+notation "[term 19 a,term 19 b]" non associative with precedence 90 for @{'segment $a $b}.
 interpretation "Ordered set sergment" 'segment a b = (segment _ a b).
 
-notation "hvbox(x \in break [a,b])" non associative with precedence 45 
+notation "hvbox(x \in break [term 19 a, term 19 b])" non associative with precedence 45 
   for @{'segment_in $a $b $x}.
 interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).