minimize theory imports
authorhuffman
Sat Oct 02 17:50:33 2010 -0700 (2010-10-02)
changeset 399671c6dce3ef477
parent 39966 20c74cf9c112
child 39968 d841744718fe
minimize theory imports
src/HOLCF/Algebraic.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/Completion.thy
     1.1 --- a/src/HOLCF/Algebraic.thy	Fri Oct 01 07:40:57 2010 -0700
     1.2 +++ b/src/HOLCF/Algebraic.thy	Sat Oct 02 17:50:33 2010 -0700
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Algebraic deflations *}
     1.5  
     1.6  theory Algebraic
     1.7 -imports Completion Fix Eventual
     1.8 +imports Completion Fix Eventual Bifinite
     1.9  begin
    1.10  
    1.11  subsection {* Constructing finite deflations by iteration *}
     2.1 --- a/src/HOLCF/CompactBasis.thy	Fri Oct 01 07:40:57 2010 -0700
     2.2 +++ b/src/HOLCF/CompactBasis.thy	Sat Oct 02 17:50:33 2010 -0700
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Compact bases of domains *}
     2.5  
     2.6  theory CompactBasis
     2.7 -imports Completion
     2.8 +imports Completion Bifinite
     2.9  begin
    2.10  
    2.11  subsection {* Compact bases of bifinite domains *}
     3.1 --- a/src/HOLCF/Completion.thy	Fri Oct 01 07:40:57 2010 -0700
     3.2 +++ b/src/HOLCF/Completion.thy	Sat Oct 02 17:50:33 2010 -0700
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Defining bifinite domains by ideal completion *}
     3.5  
     3.6  theory Completion
     3.7 -imports Bifinite
     3.8 +imports Cfun
     3.9  begin
    3.10  
    3.11  subsection {* Ideals over a preorder *}