| changeset 72812 | caf2fd14e28b |
| parent 72808 | ba65dc3e35af |
| child 72910 | c145be662fbd |
--- 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>