X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fprevalued_lattice.ma;h=d41a9a92234f24078e33241579d852ffcd9fb8c9;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=bf4a26643b5272cfc413c929f12325c95ed5d20c;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma
index bf4a26643..d41a9a922 100644
--- a/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma
@@ -34,15 +34,15 @@ record vlattice (R : togroup) : Type ≝ {
   meet_join_le: ∀x,y,z.  value (meet x y) ≤ value (meet x (join y z)) 
 }. 
 
-interpretation "valued lattice meet" 'and a b = (meet _ _ a b).
+interpretation "valued lattice meet" 'and a b = (meet ? ? a b).
 
-interpretation "valued lattice join" 'or a b = (join _ _ a b).
+interpretation "valued lattice join" 'or a b = (join ? ? a b).
  
 notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}.
-interpretation "lattice value" 'value2 a = (value _ _ a).
+interpretation "lattice value" 'value2 a = (value ? ? a).
 
 notation "\mu" non associative with precedence 80 for @{ 'value }.
-interpretation "lattice value" 'value = (value _ _).
+interpretation "lattice value" 'value = (value ? ?).
 
 lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L. 
   μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).