1.1 --- a/src/HOL/Word/WordBitwise.thy	Mon Apr 27 10:11:46 2009 +0200
     1.2 +++ b/src/HOL/Word/WordBitwise.thy	Mon Apr 27 11:27:19 2009 +0200
     1.3 @@ -443,8 +443,10 @@
     1.4  
     1.5  lemmas test_bit_2p = refl [THEN test_bit_2p', unfolded word_size]
     1.6  
     1.7 -lemmas nth_w2p = test_bit_2p [unfolded of_int_number_of_eq
     1.8 -  word_of_int [symmetric] Int.of_int_power]
     1.9 +lemma nth_w2p:
    1.10 +  "((2\<Colon>'a\<Colon>len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a\<Colon>len)"
    1.11 +  unfolding test_bit_2p [symmetric] word_of_int [symmetric]
    1.12 +  by (simp add:  of_int_power)
    1.13  
    1.14  lemma uint_2p: 
    1.15    "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"