# HG changeset patch
# User huffman
# Date 1324552466 -3600
# Node ID ed9cc0634aafecf5c946cd78893aa907385bbb80
# Parent  e49e45fee615ad4cc6391123163f37f6c0e93c3c
add lemma bin_nth_minus1

diff -r e49e45fee615 -r ed9cc0634aaf src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 21 18:23:08 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Dec 22 12:14:26 2011 +0100
@@ -275,6 +275,9 @@
 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
   by (induct n) auto
 
+lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
+  by (induct n) auto
+
 lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
   by (induct n) auto