
diff -r 24f563d94497 -r cbb6f2243b52 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 19:21:36 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 14:02:02 2011 +0100
@@ -269,6 +269,9 @@
 lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
   by (auto intro!: bin_nth_lem del: equalityI)
 
+lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
+  by (induct n) auto
+
 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
   by (induct n) auto
 




