X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=aa2d6704bf50bce5b1b52668ccb44c286c5cc9d7;hb=eaaea3c18083de3e442e939768ff450d3b093911;hp=d6043fba2c1d413fc22626fd567e18dbc34c5779;hpb=dc66c8d89a5147178ccdacb8341ed26c9c52f06b;p=helm.git

diff --git a/matita/matita/nlibrary/topology/igft.ma b/matita/matita/nlibrary/topology/igft.ma
index d6043fba2..aa2d6704b 100644
--- a/matita/matita/nlibrary/topology/igft.ma
+++ b/matita/matita/nlibrary/topology/igft.ma
@@ -781,7 +781,7 @@ D*)
 
 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 
-notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
+notation "◃U" non associative with precedence 60 for @{ 'coverage $U }.
 
 interpretation "coverage cover" 'coverage U = (coverage ? U).
 
@@ -826,7 +826,7 @@ the biggest solution for such equation.
 
 D*) 
 
-notation "⋉F" non associative with precedence 55
+notation "⋉F" non associative with precedence 60
 for @{ 'fished $F }.
 
 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
@@ -1039,8 +1039,8 @@ ninductive Ord (A : nAx) : Type[0] ≝
  | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
 
 notation "0" non associative with precedence 90 for @{ 'oO }.
-notation "x+1" non associative with precedence 50 for @{'oS $x }.
-notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
+notation "x+1" non associative with precedence 55 for @{'oS $x }.
+notation "Λ term 90 f" non associative with precedence 55 for @{ 'oL $f }.
 
 interpretation "ordinals Zero" 'oO = (oO ?).
 interpretation "ordinals Succ" 'oS x = (oS ? x).
@@ -1068,8 +1068,8 @@ nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
   | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n} 
   | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
   
-notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
-notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
+notation < "term 90 U \sub (term 90 x)" non associative with precedence 55 for @{ 'famU $U $x }.
+notation > "U ⎽ term 90 x" non associative with precedence 55 for @{ 'famU $U $x }.
 
 interpretation "famU" 'famU U x = (famU ? U x).