# HG changeset patch
# User nipkow
# Date 1564556640 -7200
# Node ID 7c2724cefcb8bf545fb9c2169b2ce55aeb4f9bb1
# Parent  6e34025981beaf8337a52fe643c7633791a66a7e
reduced dependencies

diff -r 6e34025981be -r 7c2724cefcb8 src/HOL/Data_Structures/Binomial_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
diff -r 6e34025981be -r 7c2724cefcb8 src/HOL/Data_Structures/Leftist_Heap.thy
--- 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