src/HOL/Data_Structures/Binomial_Heap.thy
changeset 72812 caf2fd14e28b
parent 72808 ba65dc3e35af
child 72910 c145be662fbd
equal deleted inserted replaced
72809:64d8a7e6d8fa 72812:caf2fd14e28b
     6 
     6 
     7 theory Binomial_Heap
     7 theory Binomial_Heap
     8 imports
     8 imports
     9   "HOL-Library.Pattern_Aliases"
     9   "HOL-Library.Pattern_Aliases"
    10   Complex_Main
    10   Complex_Main
    11   "HOL-Data_Structures.Priority_Queue_Specs"
    11   Priority_Queue_Specs
    12 begin
    12 begin
    13 
    13 
    14 text \<open>
    14 text \<open>
    15   We formalize the binomial heap presentation from Okasaki's book.
    15   We formalize the binomial heap presentation from Okasaki's book.
    16   We show the functional correctness and complexity of all operations.
    16   We show the functional correctness and complexity of all operations.