[isabelle-dev] Towards the next release

[Christian Sternagel]

Dear all,

in preparation for the next release I refactored one of our AFP entries 
(Abstract-Rewriting). There was an underlying theory Util.thy (quite 
big), which essentially turned out to be unused in the rest of the AFP 
entry ;) (but we heavily rely on it in IsaFoR, which is not in the AFP).

While refactoring I saw that some lemmas from Util.thy have found their 
way (either by moving or independently) into the main Isabelle 
distribution (mostly List.thy) -- but without being removed from the AFP 
entry.

Still there are many definitions and lemmas left that are not part of 
the main distribution (some of which are ugly and ad hoc, but others 
quite useful and maybe deserving to end up in the distribution or library).

After this rather long story ;) my actual question: Is there some way to 
propose definitions/lemmas for the main distribution/library? If not, 
maybe someone of the developers feels like reading through the attached 
theory-file and picking out whatever he/she likes?

cheers

chris

On 02/28/2012 10:21 PM, Makarius wrote:
> Dear all,
>
> 4 months after Isabelle2011-1 we are roughly in the middle between two
> official releases. This is a good point to recollect things for the
> coming release, better than a few weeks before actual rollout (which
> will the time for testing the integrated system, not adding new features).
>
> After 3.4 weeks vacation in Marokko in Jan/Feb and 2 weeks working
> through my mail folders like crazy, I still have issues in the pipeline
> that need to be reanimated. I also need to figure out which essential
> things of the Prover IDE can make it into the release ...
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Collect.thy
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120316/15990b0b/attachment-0002.ksh>