*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Replacing Integration by Multivariate_Analysis*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 23 Feb 2010 16:58:28 +0100*Cc*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, Robert Himmelmann <himmelma at in.tum.de>, Johannes Hölzl <hoelzl at in.tum.de>, Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <cc2478ab1002230743v196bbe37y87f8e1bb0c902559@mail.gmail.com>*References*: <1266327830.2234.556.camel@macbroy12.informatik.tu-muenchen.de> <4B7B977B.4090809@informatik.tu-muenchen.de> <cc2478ab1002230743v196bbe37y87f8e1bb0c902559@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.23 (Macintosh/20090812)

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

**Follow-Ups**:**Re: [isabelle] Replacing Integration by Multivariate_Analysis***From:*Johannes Hölzl

**References**:**[isabelle] Replacing Integration by Multivariate_Analysis***From:*Johannes Hölzl

**Re: [isabelle] Replacing Integration by Multivariate_Analysis***From:*Florian Haftmann

**Re: [isabelle] Replacing Integration by Multivariate_Analysis***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Replacing Integration by Multivariate_Analysis
- Next by Date: Re: [isabelle] Replacing Integration by Multivariate_Analysis
- Previous by Thread: Re: [isabelle] Replacing Integration by Multivariate_Analysis
- Next by Thread: Re: [isabelle] Replacing Integration by Multivariate_Analysis
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list