| changeset 40086 | c339c0e8fdfb |
| parent 40012 | f13341a45407 |
| child 40484 | 768f7e264e2b |
--- a/src/HOLCF/Bifinite.thy Thu Oct 21 15:19:07 2010 -0700 +++ b/src/HOLCF/Bifinite.thy Thu Oct 21 15:21:39 2010 -0700 @@ -5,7 +5,7 @@ header {* Bifinite domains *} theory Bifinite -imports Algebraic Cprod Sprod Ssum Up Lift One Tr +imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable begin subsection {* Class of bifinite domains *}