Re: [isabelle] Replacing Integration by Multivariate_Analysis

On Tue, Feb 16, 2010 at 11:15 PM, Florian Haftmann
<florian.haftmann at> wrote:
>> 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.
> Sounds reasonable to me.  Perhaps the old Integral could go to a theory
> in ex/?
>        Florian

I agree that the old Integral should be kept somewhere, like in HOL/ex.

Johannes and Robert: I thought your plan was just to remove it from
the Isabelle/HOL image (which I fully approve of), but now it is
completely gone!

It is probably best to handle little-used libraries in a more
conservative way, like first moving them to a different directory,
rather than just deleting them completely. Libraries may have value
even if nobody imports them: I think Integral.thy is a fairly readable
exposition of gauge integrals (especially when compared to
Multivariate_Analysis!), and would be a useful object of study for
someone trying to learn the subject. I'll take responsibility for
maintaining the theory, if maintenance is a concern.

- Brian

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