equal
deleted
inserted
replaced
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. |