[isabelle-dev] priority queues

Makarius makarius at sketis.net
Sat Oct 27 16:58:22 CEST 2012

On Wed, 24 Oct 2012, Lukas Bulwahn wrote:

> I think priority queues are roughly ordered lists (the priority is the 
> ordering). So, you could have a look at Pure/General/ord_list.ML

The main virtue of Ord_List is that insert and merge are of the same 
complexity: linear.  This is important in special applications like 
maintaining the hyps field of a thm efficiently, but in most other 
applications the linearity of insert is a performance trap.  The balanced 
tree structure underlying module Table works better in general.


More information about the isabelle-dev mailing list