# HG changeset patch
# User huffman
# Date 1140311487 -3600
# Node ID 3aabd46340e03f2cef73af398f64da83289789cd
# Parent  7d69b6d7b8f196e37b59fa7b81bd39038b76b1c0
use minimal imports

diff -r 7d69b6d7b8f1 -r 3aabd46340e0 src/HOLCF/Discrete.thy
--- 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"
diff -r 7d69b6d7b8f1 -r 3aabd46340e0 src/HOLCF/HOLCF.thy
--- 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"
diff -r 7d69b6d7b8f1 -r 3aabd46340e0 src/HOLCF/Porder.thy
--- 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 *}
diff -r 7d69b6d7b8f1 -r 3aabd46340e0 src/HOLCF/Up.thy
--- 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