| changeset 261 | 34fb63221536 |
| parent 239 | 02b14a21761a |
| child 262 | 9279f95e574a |
| 259:22c199522bef | 261:34fb63221536 |
|---|---|
17 quotient_def (for my_int) |
17 quotient_def (for my_int) |
18 ZERO::"my_int" |
18 ZERO::"my_int" |
19 where |
19 where |
20 "ZERO \<equiv> (0::nat, 0::nat)" |
20 "ZERO \<equiv> (0::nat, 0::nat)" |
21 |
21 |
22 thm ZERO_def |
|
23 |
22 |
24 quotient_def (for my_int) |
23 quotient_def (for my_int) |
25 ONE::"my_int" |
24 ONE::"my_int" |
26 where |
25 where |
27 "ONE \<equiv> (1::nat, 0::nat)" |
26 "ONE \<equiv> (1::nat, 0::nat)" |