author | Peter Lammich |
Fri, 04 Dec 2020 17:55:17 +0000 | |
changeset 72813 | b09f358f3eb0 |
parent 72812 | caf2fd14e28b (diff) |
parent 72811 | ef21a1de340d (current diff) |
child 72828 | 18bc50e58e38 |
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Fri Dec 04 18:30:00 2020 +0100 +++ b/src/HOL/Data_Structures/Binomial_Heap.thy Fri Dec 04 17:55:17 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>