nasty change in the lexer/parser:

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

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 da3299b649d61c8f3da1ea52f5f806934d1485e2..857b2d1699daec9429a5aa6b100a6c1f570665c0 100644 (file)
--- 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.