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

diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma b/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma
index 71fe1a81b..4c4602c8b 100644
--- a/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma
@@ -30,7 +30,7 @@ record vector_space (K:field): Type \def
   vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult
 }.
 
-interpretation "Vector space external product" 'times a b = (emult _ _ a b).
+interpretation "Vector space external product" 'times a b = (emult ? ? a b).
 
 record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def
  { sn_positive: ∀x:V. zero R ≤ semi_norm x;