| changeset 40502 | 8e92772bc0e8 |
| parent 40497 | d2e876d6da8c |
| child 40506 | 4c5363173f88 |
| 40501:2ed71459136e | 40502:8e92772bc0e8 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Bifinite domains *} |
5 header {* Bifinite domains *} |
6 |
6 |
7 theory Bifinite |
7 theory Bifinite |
8 imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable |
8 imports Algebraic Map_Functions Countable |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Class of bifinite domains *} |
11 subsection {* Class of bifinite domains *} |
12 |
12 |
13 text {* |
13 text {* |