# HG changeset patch
# User huffman
# Date 1286067033 25200
# Node ID 1c6dce3ef477fb929bf4303ea5f8ad138a6d7ad5
# Parent  20c74cf9c112826b3bd2ba180492ce9d8fcb8c1f
minimize theory imports

diff -r 20c74cf9c112 -r 1c6dce3ef477 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Fri Oct 01 07:40:57 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Sat Oct 02 17:50:33 2010 -0700
@@ -5,7 +5,7 @@
 header {* Algebraic deflations *}
 
 theory Algebraic
-imports Completion Fix Eventual
+imports Completion Fix Eventual Bifinite
 begin
 
 subsection {* Constructing finite deflations by iteration *}
diff -r 20c74cf9c112 -r 1c6dce3ef477 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Oct 01 07:40:57 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy	Sat Oct 02 17:50:33 2010 -0700
@@ -5,7 +5,7 @@
 header {* Compact bases of domains *}
 
 theory CompactBasis
-imports Completion
+imports Completion Bifinite
 begin
 
 subsection {* Compact bases of bifinite domains *}
diff -r 20c74cf9c112 -r 1c6dce3ef477 src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Fri Oct 01 07:40:57 2010 -0700
+++ b/src/HOLCF/Completion.thy	Sat Oct 02 17:50:33 2010 -0700
@@ -5,7 +5,7 @@
 header {* Defining bifinite domains by ideal completion *}
 
 theory Completion
-imports Bifinite
+imports Cfun
 begin
 
 subsection {* Ideals over a preorder *}