| changeset 60429 | d3d1e185cd63 |
| parent 60352 | d46de31a50c4 |
| child 60500 | 903bb1495239 |
--- a/src/HOL/Library/Bit.thy Thu Jun 11 21:41:55 2015 +0100 +++ b/src/HOL/Library/Bit.thy Fri Jun 12 08:53:23 2015 +0200 @@ -117,7 +117,7 @@ "inverse x = (x :: bit)" definition divide_bit_def [simp]: - "divide x y = (x * y :: bit)" + "x div y = (x * y :: bit)" lemmas field_bit_defs = plus_bit_def times_bit_def minus_bit_def uminus_bit_def