X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fnlibrary%2Ftopology%2Figft-setoid.ma;h=15c3320f20e36a25007ef04e7b5d73cb9be5e97a;hb=cbcadc678c098f64e7eac31cb73297558ba37b4a;hp=a4d833cae0007f8f7d78f3a888107357c1274292;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/nlibrary/topology/igft-setoid.ma b/matita/matita/nlibrary/topology/igft-setoid.ma
index a4d833cae..15c3320f2 100644
--- a/matita/matita/nlibrary/topology/igft-setoid.ma
+++ b/matita/matita/nlibrary/topology/igft-setoid.ma
@@ -25,7 +25,7 @@ nrecord category : Type[2] ≝
    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
  }.
 
-notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
+notation "hvbox(A break ⇒ B)" right associative with precedence 55 for @{ 'arrows $A $B }.
 interpretation "arrows" 'arrows A B = (unary_morphism A B).
 
 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
@@ -162,8 +162,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 "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
-notation "x+1" non associative with precedence 50 for @{'oS $x }.
+notation "Λ term 90 f" non associative with precedence 55 for @{ 'oL $f }.
+notation "x+1" non associative with precedence 55 for @{'oS $x }.
 
 interpretation "ordinals Zero" 'oO = (oO ?).
 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
@@ -194,8 +194,8 @@ nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝
                   
 (*    
   
-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).