[isabelle] Replacing Integration by Multivariate_Analysis



Hi Isabelle Users,

Robert Himmelmann is currently porting the Multivariate Analysis from
HOL-light to Isabelle/HOL. This contains a definition of the Gauge
Integral. However a one-dimensional version of this is already in
src/HOL/Integration.

To avoid a duplication of maintenance we plan to remove the current
one-dimensional Integral definition and replace it by a definition based
on Multivariate Analysis. Therefore users of the old Integral need to
adjust their proofs and import the HOL-Multivariate_Analysis image in
the future.

Is there anyone using the old Integral? There is no usage in Isabelle or
the AFP. Are there any objections or comments?

Best Regards,
 - Johannes

PS: Also Armin Heller and I currently port the Probability theory from
HOL4, which contains the Lebegues integration (based again on
afp/thy/Integration). Hence in the future will be at least two integrals
in Isabelle/HOL anyway. Hopefully we can show the equivalence of both
integrals when the function if Gauge and Lebegues integrable.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.