src/HOLCF/HOLCF.thy
changeset 19105 3aabd46340e0
parent 17923 18c66ca0c776
child 23152 9497234a2743
--- a/src/HOLCF/HOLCF.thy	Sun Feb 19 01:40:13 2006 +0100
+++ b/src/HOLCF/HOLCF.thy	Sun Feb 19 02:11:27 2006 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory HOLCF
-imports Sprod Ssum Up Lift Discrete One Tr Domain
+imports Sprod Ssum Up Lift Discrete One Tr Domain Main
 uses
   "holcf_logic.ML"
   "cont_consts.ML"