| changeset 36349 | 39be26d1bc28 |
| parent 31212 | a94aea0cef76 |
| child 36409 | d323e7773aa8 |
| 36348:89c54f51f55a | 36349:39be26d1bc28 |
|---|---|
47 by (induct x) simp_all |
47 by (induct x) simp_all |
48 |
48 |
49 |
49 |
50 subsection {* Type @{typ bit} forms a field *} |
50 subsection {* Type @{typ bit} forms a field *} |
51 |
51 |
52 instantiation bit :: "{field, division_by_zero}" |
52 instantiation bit :: "{field, division_ring_inverse_zero}" |
53 begin |
53 begin |
54 |
54 |
55 definition plus_bit_def: |
55 definition plus_bit_def: |
56 "x + y = bit_case y (bit_case 1 0 y) x" |
56 "x + y = bit_case y (bit_case 1 0 y) x" |
57 |
57 |