diff -r 89c54f51f55a -r 39be26d1bc28 src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Mon Apr 26 11:34:15 2010 +0200 +++ b/src/HOL/Library/Bit.thy Mon Apr 26 11:34:17 2010 +0200 @@ -49,7 +49,7 @@ subsection {* Type @{typ bit} forms a field *} -instantiation bit :: "{field, division_by_zero}" +instantiation bit :: "{field, division_ring_inverse_zero}" begin definition plus_bit_def: