X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Figft%2Figft.ma;h=902ad692f76de5f02ada7378a7122653e10baab7;hb=bf816f05ddbe0ded4948dd33490619724dc4f7cf;hp=5fda9145465f6c1e35b95b452c0c90be72d355e4;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/contribs/igft/igft.ma b/matita/matita/contribs/igft/igft.ma
index 5fda91454..902ad692f 100644
--- a/matita/matita/contribs/igft/igft.ma
+++ b/matita/matita/contribs/igft/igft.ma
@@ -1,8 +1,8 @@
 
 record powerset (A : Type) : Type := { content : A → CProp }.
 
-notation > "Ω ^ A" non associative with precedence 50 for @{'P $A}.
-notation "Ω \sup A" non associative with precedence 50 for @{'P $A}.
+notation > "Ω ^ A" non associative with precedence 55 for @{'P $A}.
+notation "Ω \sup A" non associative with precedence 55 for @{'P $A}.
 interpretation "Powerset" 'P A = (powerset A).
 
 record AxiomSet : Type := {
@@ -30,7 +30,7 @@ interpretation "C a i" 'C2 a i = (C_ ? a i).
 definition in_subset :=
   λA:AxiomSet.λa∈A.λU:Ω^A.content A U a.
   
-notation "hvbox(a break εU)" non associative with precedence 50 for 
+notation "hvbox(a break εU)" non associative with precedence 55 for 
 @{'in_subset $a $U}.
 interpretation "In subset" 'in_subset a U = (in_subset ? a U).