Re: [isabelle] Replacing Integration by Multivariate_Analysis



I sympathize with Brian's sentiments. But when you put the theory into
HOL/ex
1. include a comment that states clearly that this is of
historical/expository interest only and that HOL's proper integration
theory is found elsewhere.
2. Remove extraneous stuff, in this case the lemmas beyond FCT1.

Tobias


Brian Huffman schrieb:
> On Tue, Feb 16, 2010 at 11:15 PM, Florian Haftmann
> <florian.haftmann at informatik.tu-muenchen.de> 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.