| changeset 11704 | 3c50a2cd6f00 |
| parent 11701 | 3d51fbf81c17 |
| child 15354 | 9234f5765d9c |
| 11703:6e5de8d4290a | 11704:3c50a2cd6f00 |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 EvenOdd = Misc + |
9 EvenOdd = Misc + |
10 |
10 |
11 constdefs even :: nat => bool |
11 constdefs even :: nat => bool |
12 "even n == # 2 dvd n" |
12 "even n == 2 dvd n" |
13 |
13 |
14 consts |
14 consts |
15 Even, Odd :: pname |
15 Even, Odd :: pname |
16 rules |
16 rules |
17 Even_neq_Odd "Even ~= Odd" |
17 Even_neq_Odd "Even ~= Odd" |