author | Peter Lammich |
Fri, 04 Dec 2020 17:54:57 +0000 | |
changeset 72812 | caf2fd14e28b |
parent 72809 | 64d8a7e6d8fa |
child 72813 | b09f358f3eb0 |
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Fri Dec 04 17:21:09 2020 +0000 +++ b/src/HOL/Data_Structures/Binomial_Heap.thy Fri Dec 04 17:54:57 2020 +0000 @@ -8,7 +8,7 @@ imports "HOL-Library.Pattern_Aliases" Complex_Main - "HOL-Data_Structures.Priority_Queue_Specs" + Priority_Queue_Specs begin text \<open>