--- a/src/HOLCF/Discrete.thy Sun Feb 19 01:40:13 2006 +0100
+++ b/src/HOLCF/Discrete.thy Sun Feb 19 02:11:27 2006 +0100
@@ -8,7 +8,7 @@
header {* Discrete cpo types *}
theory Discrete
-imports Cont Datatype
+imports Cont
begin
datatype 'a discr = Discr "'a :: type"
--- 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"
--- a/src/HOLCF/Porder.thy Sun Feb 19 01:40:13 2006 +0100
+++ b/src/HOLCF/Porder.thy Sun Feb 19 02:11:27 2006 +0100
@@ -6,7 +6,7 @@
header {* Partial orders *}
theory Porder
-imports Main
+imports Datatype
begin
subsection {* Type class for partial orders *}
--- a/src/HOLCF/Up.thy Sun Feb 19 01:40:13 2006 +0100
+++ b/src/HOLCF/Up.thy Sun Feb 19 02:11:27 2006 +0100
@@ -8,7 +8,7 @@
header {* The type of lifted values *}
theory Up
-imports Cfun Sum_Type Datatype
+imports Cfun
begin
defaultsort cpo