| changeset 26086 | 3c243098b64a |
| parent 25262 | d0928156e326 |
| child 29629 | 5111ce425e7a |
--- a/src/HOL/Word/Examples/WordExamples.thy Sat Feb 16 16:52:09 2008 +0100 +++ b/src/HOL/Word/Examples/WordExamples.thy Sun Feb 17 06:49:53 2008 +0100 @@ -92,7 +92,7 @@ lemma "\<not> (0b1000 :: 3 word) !! 4" by simp lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" - by (auto simp add: bin_nth_Bit) + by (auto simp add: bin_nth_Bit0 bin_nth_Bit1) lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp