<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><blockquote type="cite">Unless you refer to a particularly emerging module in some inter-release repository version --<br>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.<br></blockquote><br>I'm working on Sledgehammer with Jasmin Blanchette, so in a way this is related to the repository version of Isabelle. I'm not sure if that makes a difference, though…<br><br><blockquote type="cite">To avoid further complication, here are some hints as if this would be isabelle-users (so I refer to the latest official release):<br><br><a href="http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/heap.ML">http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/heap.ML</a><br><a href="http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/table.ML">http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/table.ML</a><br><a href="http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/graph.ML">http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/graph.ML</a><br></blockquote><br>Thanks. Jasmin already pointed me to tables. For my application, being able to use min_key as well as max_key is nice, a feature the heap structure does not seem to offer.<br><br>Steffen<div><br></div><div><br><div><div>On 27.10.2012, at 16:58, Makarius <<a href="mailto:makarius@sketis.net">makarius@sketis.net</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">On Wed, 24 Oct 2012, Lukas Bulwahn wrote:<br><br><blockquote type="cite">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<br></blockquote><br>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.<br><br><br><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br></blockquote></div><br></div></body></html>