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=11a6c88f3e717b019be2eae71711c70473b5467a;hp=53b2b0a1b9b62a8664c2c9407c17ddfd0000e9d9;hpb=c077ca16ea87ba612435a47eee714b5388204d93;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 53b2b0a1b..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,17 +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 =
- (cic:/matita/prevalued_lattice/meet.con _ _ a b).
+interpretation "valued lattice meet" 'and a b = (meet ? ? a b).
 
-interpretation "valued lattice join" 'or a b =
- (cic:/matita/prevalued_lattice/join.con _ _ 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 = (cic:/matita/prevalued_lattice/value.con _ _ a).
+interpretation "lattice value" 'value2 a = (value ? ? a).
 
 notation "\mu" non associative with precedence 80 for @{ 'value }.
-interpretation "lattice value" 'value = (cic:/matita/prevalued_lattice/value.con _ _).
+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).