| changeset 40650 | d40b347d5b0b |
| parent 40649 | dc1b5aa908ff |
| child 40651 | 9752ba7348b5 |
| 40649:dc1b5aa908ff | 40650:d40b347d5b0b |
|---|---|
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 header {* Finite types as explicit enumerations *} |
3 header {* Finite types as explicit enumerations *} |
4 |
4 |
5 theory Enum |
5 theory Enum |
6 imports Map Main |
6 imports Map String |
7 begin |
7 begin |
8 |
8 |
9 subsection {* Class @{text enum} *} |
9 subsection {* Class @{text enum} *} |
10 |
10 |
11 class enum = |
11 class enum = |