reduced dependencies
authornipkow
Wed, 31 Jul 2019 09:04:00 +0200
changeset 70450 7c2724cefcb8
parent 70449 6e34025981be
child 70451 550a5a822edb
reduced dependencies
src/HOL/Data_Structures/Binomial_Heap.thy
src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Jul 30 20:09:25 2019 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Jul 31 09:04:00 2019 +0200
@@ -6,7 +6,7 @@
 
 theory Binomial_Heap
 imports
-  Base_FDS
+  "HOL-Library.Pattern_Aliases"
   Complex_Main
   Priority_Queue_Specs
 begin
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Tue Jul 30 20:09:25 2019 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Jul 31 09:04:00 2019 +0200
@@ -4,7 +4,7 @@
 
 theory Leftist_Heap
 imports
-  Base_FDS
+  "HOL-Library.Pattern_Aliases"
   Tree2
   Priority_Queue_Specs
   Complex_Main