src/HOLCF/HOLCF.thy

--- a/src/HOLCF/HOLCF.thy	Tue Dec 16 09:10:09 2008 -0800
+++ b/src/HOLCF/HOLCF.thy	Tue Dec 16 09:44:59 2008 -0800
@@ -6,7 +6,8 @@
 *)
 
 theory HOLCF
-imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Algebraic Universal Main
+imports
+  Domain ConvexPD Algebraic Universal Dsum Main
 uses
   "holcf_logic.ML"
   "Tools/cont_consts.ML"