# HG changeset patch
# User huffman
# Date 1287699699 25200
# Node ID c339c0e8fdfb71c35ad108a9662b7f39bca1b9d7
# Parent  c157ff4d59a6e6e12a952c271a578cea3d3f3772
minimize imports

diff -r c157ff4d59a6 -r c339c0e8fdfb src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Thu Oct 21 15:19:07 2010 -0700
+++ b/src/HOLCF/Bifinite.thy	Thu Oct 21 15:21:39 2010 -0700
@@ -5,7 +5,7 @@
 header {* Bifinite domains *}
 
 theory Bifinite
-imports Algebraic Cprod Sprod Ssum Up Lift One Tr
+imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable
 begin
 
 subsection {* Class of bifinite domains *}
diff -r c157ff4d59a6 -r c339c0e8fdfb src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Thu Oct 21 15:19:07 2010 -0700
+++ b/src/HOLCF/Lift.thy	Thu Oct 21 15:21:39 2010 -0700
@@ -5,7 +5,7 @@
 header {* Lifting types of class type to flat pcpo's *}
 
 theory Lift
-imports Discrete Up Countable
+imports Discrete Up
 begin
 
 default_sort type