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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > This body part will be downloaded on demand. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev