# HG changeset patch
# User haftmann
# Date 1240824439 -7200
# Node ID ed7364584aa7119a71c2d39ab02916df169a1d3f
# Parent  bc4117fe72ab3afd77161af6a32636d89aecca26
explicit is better than implicit

diff -r bc4117fe72ab -r ed7364584aa7 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Mon Apr 27 10:11:46 2009 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Mon Apr 27 11:27:19 2009 +0200
@@ -443,8 +443,10 @@
 
 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] Int.of_int_power]
+lemma nth_w2p:
+  "((2\<Colon>'a\<Colon>len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a\<Colon>len)"
+  unfolding test_bit_2p [symmetric] word_of_int [symmetric]
+  by (simp add:  of_int_power)
 
 lemma uint_2p: 
   "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"