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

diff --git a/helm/software/matita/contribs/igft/igft.ma b/helm/software/matita/contribs/igft/igft.ma
index fb4a92340..5fda91454 100644
--- a/helm/software/matita/contribs/igft/igft.ma
+++ b/helm/software/matita/contribs/igft/igft.ma
@@ -17,22 +17,22 @@ notation > "λident a∈A.P" right associative with precedence 20
 for @{ λ${ident a} : S $A. $P }.
 
 notation "'I'" non associative with precedence 90 for @{'I}.
-interpretation "I" 'I = (I_ _).
+interpretation "I" 'I = (I_ ?).
 notation < "'I' \lpar a \rpar" non associative with precedence 90 for @{'I1 $a}.
-interpretation "I a" 'I1 a = (I_ _ a).
+interpretation "I a" 'I1 a = (I_ ? a).
 notation "'C'" non associative with precedence 90 for @{'C}.
-interpretation "C" 'C = (C_ _).
+interpretation "C" 'C = (C_ ?).
 notation < "'C' \lpar a \rpar" non associative with precedence 90 for @{'C1 $a}.
-interpretation "C a" 'C1 a = (C_ _ a).
+interpretation "C a" 'C1 a = (C_ ? a).
 notation < "'C' \lpar a , i \rpar" non associative with precedence 90 for @{'C2 $a $i}.
-interpretation "C a i" 'C2 a i = (C_ _ a i).
+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 
 @{'in_subset $a $U}.
-interpretation "In subset" 'in_subset a U = (in_subset _ a U).
+interpretation "In subset" 'in_subset a U = (in_subset ? a U).
 
 definition for_all ≝ λA:AxiomSet.λU:Ω^A.λP:A → CProp.∀x.xεU → P x.
 
@@ -41,19 +41,19 @@ inductive covers (A : AxiomSet) (U : Ω ^ A) : A → CProp :=
  | infinity_ : ∀a.∀i : I a. for_all A (C a i) (covers A U)  → covers A U a.
  
 notation "'refl'" non associative with precedence 90 for @{'refl}. 
-interpretation "refl" 'refl = (refl_ _ _ _).
+interpretation "refl" 'refl = (refl_ ? ? ?).
 
 notation "'infinity'" non associative with precedence 90 for @{'infinity}.  
-interpretation "infinity" 'infinity = (infinity_ _ _ _).
+interpretation "infinity" 'infinity = (infinity_ ? ? ?).
  
 notation "U ⊲ V" non associative with precedence 45
 for @{ 'covers_subsets $U $V}.
-interpretation "Covers subsets" 'covers_subsets U V = (for_all _ U (covers _ V)).
-interpretation "Covers elem subset" 'covers_subsets U V = (covers _ V U).
+interpretation "Covers subsets" 'covers_subsets U V = (for_all ? U (covers ? V)).
+interpretation "Covers elem subset" 'covers_subsets U V = (covers ? V U).
 
 definition subseteq := λA:AxiomSet.λU,V:Ω^A.∀x.xεU → xεV.
 
-interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
+interpretation "subseteq" 'subseteq u v = (subseteq ? u v).
 
 
 definition covers_elim_ ≝
@@ -66,7 +66,7 @@ definition covers_elim_ ≝
     in
      aux.
      
-interpretation "char" 'subset p = (mk_powerset _ p).  
+interpretation "char" 'subset p = (mk_powerset ? p).  
      
 definition covers_elim : 
  ∀A:AxiomSet.∀U: Ω^A.∀P:A→CProp.∀H1: U ⊆ {x | P x}. 
@@ -85,5 +85,5 @@ theorem trans_: ∀A:AxiomSet.∀a∈A.∀U,V. a ⊲ U → U ⊲ V → a ⊲ V.
 qed.
 
 notation "'trans'" non associative with precedence 90 for @{'trans}. 
-interpretation "trans" 'trans = (trans_ _ _).
+interpretation "trans" 'trans = (trans_ ? ?).