| changeset 39967 | 1c6dce3ef477 |
| parent 36635 | 080b755377c0 |
| child 39974 | b525988432e9 |
| 39966:20c74cf9c112 | 39967:1c6dce3ef477 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Compact bases of domains *} |
5 header {* Compact bases of domains *} |
6 |
6 |
7 theory CompactBasis |
7 theory CompactBasis |
8 imports Completion |
8 imports Completion Bifinite |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Compact bases of bifinite domains *} |
11 subsection {* Compact bases of bifinite domains *} |
12 |
12 |
13 default_sort profinite |
13 default_sort profinite |