X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fintegration_algebras.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Fintegration_algebras.ma;h=dc0ad9d3277cd1274da16cc8caa748e92b77aa2a;hb=75b9cb11f623690c135dfe39b84065887f3f0f79;hp=46bebc0e9da6745255d64691b99f5fe6a00eb7e2;hpb=9408f2869ddbbbae68dcb23ebf6c358c61888d0d;p=helm.git

diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma
index 46bebc0e9..dc0ad9d32 100644
--- a/helm/software/matita/dama/integration_algebras.ma
+++ b/helm/software/matita/dama/integration_algebras.ma
@@ -146,7 +146,7 @@ record integration_riesz_space (R:real) : Type \def
          ) * irs_unit))) 0;
    irs_quotient_space1:
     ∀f,g:irs_archimedean_riesz_space.
-     integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g
+     integral (absolute_value irs_archimedean_riesz_space (f - g)) = 0 → f=g
  }.
 
 definition induced_norm_fun ≝