src/HOLCF/HOLCF.thy
changeset 35473 c4d3d65856dd
parent 33588 ea9becc59636
child 35906 e0382e4b4da7
--- a/src/HOLCF/HOLCF.thy	Sun Feb 28 14:05:21 2010 -0800
+++ b/src/HOLCF/HOLCF.thy	Sun Feb 28 14:55:42 2010 -0800
@@ -6,8 +6,10 @@
 
 theory HOLCF
 imports
-  Domain ConvexPD Algebraic Universal Sum_Cpo Main
-  Representable
+  Main
+  Domain
+  Powerdomains
+  Sum_Cpo
 uses
   "holcf_logic.ML"
   "Tools/adm_tac.ML"