# HG changeset patch # User Peter Lammich # Date 1607104497 0 # Node ID caf2fd14e28b913d1982830c087e1a5072e7d634 # Parent 64d8a7e6d8fa596c6272222523fa0cbdfe91a9b5 removed session name diff -r 64d8a7e6d8fa -r caf2fd14e28b src/HOL/Data_Structures/Binomial_Heap.thy --- 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 \