changeset 48926 | 8d7778a19857 |
parent 37765 | 26bdfb7b680b |
child 51160 | 599ff65b85e2 |
48925:9c9bbaa2fff1 | 48926:8d7778a19857 |
---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Order on characters *} |
5 header {* Order on characters *} |
6 |
6 |
7 theory Char_ord |
7 theory Char_ord |
8 imports Product_ord Char_nat Main |
8 imports Char_nat |
9 begin |
9 begin |
10 |
10 |
11 instantiation nibble :: linorder |
11 instantiation nibble :: linorder |
12 begin |
12 begin |
13 |
13 |