[isabelle-dev] Towards the next release

[Christian Sternagel]

Something slightly related and not very important. In changeset 
9ff441f295c2 of the Isabelle repo the congruence rule for the constant 
"list_ex" is called list_any_cong. For consistency I suggest to rename 
it to list_ex_cong.

cheers

chris

On 03/16/2012 06:47 PM, Christian Sternagel wrote:
> 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
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev