use minimal imports
authorhuffman
Sun Feb 19 02:11:27 2006 +0100 (2006-02-19)
changeset 191053aabd46340e0
parent 19104 7d69b6d7b8f1
child 19106 6e6b5b1fdc06
use minimal imports
src/HOLCF/Discrete.thy
src/HOLCF/HOLCF.thy
src/HOLCF/Porder.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Discrete.thy	Sun Feb 19 01:40:13 2006 +0100
     1.2 +++ b/src/HOLCF/Discrete.thy	Sun Feb 19 02:11:27 2006 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Discrete cpo types *}
     1.5  
     1.6  theory Discrete
     1.7 -imports Cont Datatype
     1.8 +imports Cont
     1.9  begin
    1.10  
    1.11  datatype 'a discr = Discr "'a :: type"
     2.1 --- a/src/HOLCF/HOLCF.thy	Sun Feb 19 01:40:13 2006 +0100
     2.2 +++ b/src/HOLCF/HOLCF.thy	Sun Feb 19 02:11:27 2006 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  *)
     2.5  
     2.6  theory HOLCF
     2.7 -imports Sprod Ssum Up Lift Discrete One Tr Domain
     2.8 +imports Sprod Ssum Up Lift Discrete One Tr Domain Main
     2.9  uses
    2.10    "holcf_logic.ML"
    2.11    "cont_consts.ML"
     3.1 --- a/src/HOLCF/Porder.thy	Sun Feb 19 01:40:13 2006 +0100
     3.2 +++ b/src/HOLCF/Porder.thy	Sun Feb 19 02:11:27 2006 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Partial orders *}
     3.5  
     3.6  theory Porder
     3.7 -imports Main
     3.8 +imports Datatype
     3.9  begin
    3.10  
    3.11  subsection {* Type class for partial orders *}
     4.1 --- a/src/HOLCF/Up.thy	Sun Feb 19 01:40:13 2006 +0100
     4.2 +++ b/src/HOLCF/Up.thy	Sun Feb 19 02:11:27 2006 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  header {* The type of lifted values *}
     4.5  
     4.6  theory Up
     4.7 -imports Cfun Sum_Type Datatype
     4.8 +imports Cfun
     4.9  begin
    4.10  
    4.11  defaultsort cpo