| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15251 | bb6f072c8d10 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Parity: Even and Odd for ints and nats*} |
6 header {* Parity: Even and Odd for ints and nats*} |
7 |
7 |
8 theory Parity |
8 theory Parity |
9 import Divides IntDiv NatSimprocs |
9 imports Divides IntDiv NatSimprocs |
10 begin |
10 begin |
11 |
11 |
12 axclass even_odd < type |
12 axclass even_odd < type |
13 |
13 |
14 instance int :: even_odd .. |
14 instance int :: even_odd .. |