diff -r 82dd239e0f65 -r 8b1c0d434824 src/HOL/Word/WordShift.thy --- a/src/HOL/Word/WordShift.thy Tue Jan 15 16:19:21 2008 +0100 +++ b/src/HOL/Word/WordShift.thy Tue Jan 15 16:19:23 2008 +0100 @@ -483,7 +483,7 @@ lemma mask_bl: "mask n = of_bl (replicate n True)" by (auto simp add : test_bit_of_bl word_size intro: word_eqI) -lemma mask_bin: "mask n = number_of (bintrunc n Numeral.Min)" +lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)" by (auto simp add: nth_bintr word_size intro: word_eqI) lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"