| changeset 197 | ca4ddf26a7c7 |
| parent 63 | b620a2a0806a |
| 196:704fd8749dad | 197:ca4ddf26a7c7 |
|---|---|
1 header {* Order on product types *} |
|
2 |
|
3 theory Precedence_ord |
1 theory Precedence_ord |
4 imports Main |
2 imports Main |
5 begin |
3 begin |
4 |
|
5 section {* Order on product types *} |
|
6 |
6 |
7 datatype precedence = Prc nat nat |
7 datatype precedence = Prc nat nat |
8 |
8 |
9 instantiation precedence :: order |
9 instantiation precedence :: order |
10 begin |
10 begin |