[isabelle-dev] priority queues

[Makarius]

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.


 	Makarius