1.1 --- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 21 18:23:08 2011 +0100
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Thu Dec 22 12:14:26 2011 +0100
     1.3 @@ -275,6 +275,9 @@
     1.4  lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
     1.5    by (induct n) auto
     1.6  
     1.7 +lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
     1.8 +  by (induct n) auto
     1.9 +
    1.10  lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
    1.11    by (induct n) auto
    1.12