src/HOL/Word/Bit_Representation.thy

--- a/src/HOL/Word/Bit_Representation.thy	Thu Nov 17 08:07:54 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Nov 17 12:29:48 2011 +0100
@@ -270,6 +270,9 @@
 
 lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]
 
+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_Pls [simp]: "~ bin_nth Int.Pls n"
   by (induct n) auto