equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 subsection "Parity Analysis" |
2 |
4 |
3 theory Abs_Int1_parity |
5 theory Abs_Int1_parity |
4 imports Abs_Int1 |
6 imports Abs_Int1 |
5 begin |
7 begin |
6 |
|
7 subsection "Parity Analysis" |
|
8 |
8 |
9 datatype parity = Even | Odd | Either |
9 datatype parity = Even | Odd | Either |
10 |
10 |
11 text\<open>Instantiation of class @{class order} with type @{typ parity}:\<close> |
11 text\<open>Instantiation of class @{class order} with type @{typ parity}:\<close> |
12 |
12 |