X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fpremetric_lattice.ma;h=5c5fca20af2ed0d9ae0f1635cfae0d9de549e9af;hb=6abb01e8b00db927e16aa790354d1da57af7875b;hp=6c904055c68fbc61fa7133d35307fdab7567be93;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma
index 6c904055c..5c5fca20a 100644
--- a/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma
@@ -22,11 +22,9 @@ record premetric_lattice_ (R : todgroup) : Type ≝ {
   join: pml_carr → pml_carr → pml_carr
 }.
 
-interpretation "valued lattice meet" 'and a b =
- (cic:/matita/premetric_lattice/meet.con _ _ a b).
+interpretation "valued lattice meet" 'and a b = (meet _ _ a b).
 
-interpretation "valued lattice join" 'or a b =
- (cic:/matita/premetric_lattice/join.con _ _ a b).
+interpretation "valued lattice join" 'or a b = (join _ _ a b).
  
 record premetric_lattice_props (R : todgroup) (ml : premetric_lattice_ R) : Prop ≝ {
   prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0;
@@ -67,4 +65,4 @@ try (apply ap_symmetric; assumption); intros 4 (x y z H); change with (0 < (δ y
   apply (prop5 ? pml pml);] 
 qed.
 
-coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con.
\ No newline at end of file
+coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con.