Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Priority Queues Based on Braun ...

view this post on Zulip Email Gateway (Aug 19 2022 at 15:59):

From: Lawrence Paulson <lp15@cam.ac.uk>
"This theory implements priority queues via Braun trees. Insertion and deletion take logarithmic time and preserve the balanced nature of Braun trees.”

Many thanks to Tobias Nipkow for this entry!

Larry Paulson

Last updated: Feb 15 2026 at 05:19 UTC