[isabelle-dev] Towards the next release
c-sterna at jaist.ac.jp
Fri Mar 16 10:47:16 CET 2012
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
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?
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 ...
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the isabelle-dev