| changeset 58310 | 91ea607a34d8 |
| parent 58249 | 180f1b3508ed |
| child 61671 | 20d4cd2ceab2 |
| 58309:a09ec6daaa19 | 58310:91ea607a34d8 |
|---|---|
4 imports Abs_Int1_ITP |
4 imports Abs_Int1_ITP |
5 begin |
5 begin |
6 |
6 |
7 subsection "Parity Analysis" |
7 subsection "Parity Analysis" |
8 |
8 |
9 datatype_new parity = Even | Odd | Either |
9 datatype parity = Even | Odd | Either |
10 |
10 |
11 text{* Instantiation of class @{class preord} with type @{typ parity}: *} |
11 text{* Instantiation of class @{class preord} with type @{typ parity}: *} |
12 |
12 |
13 instantiation parity :: preord |
13 instantiation parity :: preord |
14 begin |
14 begin |