| changeset 70175 | 85fb1a585f52 |
| parent 70172 | c247bf924d25 |
| child 70183 | 3ea80c950023 |
--- a/src/HOL/Word/Bits_Int.thy Tue Apr 16 19:50:19 2019 +0000 +++ b/src/HOL/Word/Bits_Int.thy Tue Apr 16 19:50:20 2019 +0000 @@ -746,7 +746,7 @@ bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w" by (simp add: numeral_eq_Suc) -instantiation int :: bitss +instantiation int :: bits begin definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"