| changeset 26289 | 9d2c375e242b |
| parent 25350 | a5fcf6d12a53 |
| child 26558 | 7fcc10088e72 |
--- a/src/HOL/Word/WordBitwise.thy Sat Mar 15 22:07:28 2008 +0100 +++ b/src/HOL/Word/WordBitwise.thy Sat Mar 15 22:07:29 2008 +0100 @@ -443,7 +443,7 @@ lemmas test_bit_2p = refl [THEN test_bit_2p', unfolded word_size] lemmas nth_w2p = test_bit_2p [unfolded of_int_number_of_eq - word_of_int [symmetric] of_int_power] + word_of_int [symmetric] Int.of_int_power] lemma uint_2p: "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"