X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fattic%2Fintegration_algebras.ma;h=857b2d1699daec9429a5aa6b100a6c1f570665c0;hb=e1efca300fbaeb8c69a691a428a084d89a2c058f;hp=da3299b649d61c8f3da1ea52f5f806934d1485e2;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma b/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma
index da3299b64..857b2d169 100644
--- a/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma
@@ -312,7 +312,7 @@ record algebra (K: field) : Type \def
    a_algebra_properties: is_algebra ? ? a_mult a_one
  }.
 
-interpretation "Algebra product" 'times a b = (a_mult _ a b).
+interpretation "Algebra product" 'times a b = (a_mult ? a b).
 
 definition ring_of_algebra ≝
  λK.λA:algebra K.