[isabelle-dev] Some missing setup for function package in combination with Option-type

[Makarius]

On Fri, 17 Feb 2012, Lukas Bulwahn wrote:

> Just two comments:
>
> First, the discussion about this should be on the isabelle mailing list, not 
> the isabelle developer's mailing list.
> There has been a discussion just a few days ago that the developer's mailing 
> list is limited to arbitrary repository versions and the related development 
> process, including administrative things like isatest, mira etc.
>
> Second, the AFP is a perfect place to also submit small library developments. 
> The List-Index theory is such an example.
> So, the Option monad could be just turned into a small AFP entry.

I've also asked myself again this question about isabelle-users vs. 
isabelle-dev, when looking at the message for 2min, but considered it is a 
boundary case that could go either way.

In practice it is also a matter of the size of audience.  There might be 
yet unknown library contributions out there that could be joined in such 
efforts.  So there is definitely a tendency more towards isabelle-users.

(Oddly isabelle-dev appears to be much more active recently than 
isabelle-users.  Are there fewer users or fewer user problems now?)


 	Makarius