src/HOLCF/Bifinite.thy
changeset 40502 8e92772bc0e8
parent 40497 d2e876d6da8c
child 40506 4c5363173f88
     1.1 --- a/src/HOLCF/Bifinite.thy	Wed Nov 10 14:59:52 2010 -0800
     1.2 +++ b/src/HOLCF/Bifinite.thy	Wed Nov 10 17:56:08 2010 -0800
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Bifinite domains *}
     1.5  
     1.6  theory Bifinite
     1.7 -imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable
     1.8 +imports Algebraic Map_Functions Countable
     1.9  begin
    1.10  
    1.11  subsection {* Class of bifinite domains *}