| changeset 36409 | d323e7773aa8 |
| parent 36349 | 39be26d1bc28 |
| child 41959 | b460124855b8 |
--- a/src/HOL/Library/Bit.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Library/Bit.thy Mon Apr 26 15:37:50 2010 +0200 @@ -49,7 +49,7 @@ subsection {* Type @{typ bit} forms a field *} -instantiation bit :: "{field, division_ring_inverse_zero}" +instantiation bit :: field_inverse_zero begin definition plus_bit_def: