Re: [isabelle] Replacing Integration by Multivariate_Analysis



Readded the old Integration theory to HOL examples. 

It would be of course nice if someone could cleanup the proofs in this
theory and rewrite them in nice Isar-style.

- Johannes

Am Dienstag, den 23.02.2010, 16:58 +0100 schrieb Tobias Nipkow:
> 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.