[isabelle-dev] Library/List_Prefix

[Makarius]

On Mon, 3 Sep 2012, Christian Sternagel wrote:

> On 09/03/2012 08:29 AM, Gerwin Klein wrote:
>> You attached a patch, but I'm not sure anyone feels responsible for pushing 
>> it ;-)
>> 
>> Have you been working on this with someone from Munich?
> No, against my own advice ( 
> https://isabelle.in.tum.de/community/Publish_contributions_as_an_external ) I 
> haven't.
>
> The reply that got me going was the rather noncommittal:
>
> On 04/28/2012 05:05 PM, Florian Haftmann wrote:
>> Consoldiations to the library are always welcome!
>
> Until someone plucks up courage (or it is decided that my changes are 
> not worth committing) I'll keep rebasing ;)

As far as I know there is no secret commitee in the background to make 
secret decisions.  The repository clone 
http://isabelle.in.tum.de/repos/isabelle/ also shows what is in and what 
not.


Anyway, most of the usual HOL library experts are either still on 
vacation, or don't work during the nights on the weekend.

Since Library/List_Prefix was one of my responsibilities many years ago, I 
shall look at it later today, an also report back on the formal 
shortcomings of the changeset bundle that still remain.


 	Makarius