[isabelle-dev] Towards the next release

[Tobias Nipkow]

Thanks for your input, I have added some of your lemmas to List (and will write
to you about separately).

No, there is no fixed process for adding such contributions. Until it becomes a
nuisance ;-) you are welcome to post them here or send them to some active
developer.

Tobias

Am 16/03/2012 10:47, schrieb 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
> 
> 
> This body part will be downloaded on demand.