Most of the time, URIs can now be replaced with identifiers in "interpretation".

[helm.git] / helm / software / matita / contribs / dama / dama_duality / prevalued_lattice.ma

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 53b2b0a1b9b62a8664c2c9407c17ddfd0000e9d9..bf4a26643b5272cfc413c929f12325c95ed5d20c 100644 (file)
--- 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).