[isabelle-dev] priority queues

[Tobias Nipkow]

Am 27/10/2012 18:23, schrieb Makarius:
> On Sat, 27 Oct 2012, Tobias Nipkow wrote:
> 
>> Am 27/10/2012 16:55, schrieb Makarius:
>>> On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
>>>
>>>> is there an implementation of priority queues in the isabelle library?
>>>
>>> This is off-topic for this mailing list, which is for things happening around
>>> the Isabelle development process.  Unless you refer to a particularly emerging
>>> module in some inter-release repository version --
>>> lets say you are build some add-ons as very early adopter -- everything
>>> concerning Isabelle/ML programming can be discussed on the main isabelle-users
>>> mailing list.
>>
>> Steffen is a sledgehammer code developer with Jasmin and this question is not
>> appropriate for isabelle-users.
> 
> I've guessed it already.  Taking the question as such, it is perfectly normal
> Isabelle/ML user space, though.  There is no relation to inter-release
> snapshots.  The relevant modules have been stable for many years.  (Unless you
> quote a changeset where something new after Isabelle2012 has to be discussed.)

There are practically no such ML questions unrelated to theorem proving on
isabelle-users. Because 90% of the subscribers do not want and need to know
about it (thanks to Isar). The remaining 10% also subscribe to isabelle-dev. But
since the number of such questions is very small, it is not worth arguing about it.

Tobias