update in ground_2 + \lambda\delta-related ignores

[helm.git] / matita / matita / contribs / igft / igft.ma

diff --git a/matita/matita/contribs/igft/igft.ma b/matita/matita/contribs/igft/igft.ma
index 5fda9145465f6c1e35b95b452c0c90be72d355e4..902ad692f76de5f02ada7378a7122653e10baab7 100644 (file)
--- 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).