diff -r b4254b2e2b4a -r ec252975e82c src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 12:36:41 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 12:55:36 2011 +0100
@@ -43,7 +43,7 @@
   unfolding bin_last_def Bit_def
   by (cases b, simp_all add: z1pmod2)
 
-lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
+lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
   by (metis bin_rest_BIT bin_last_BIT)
 
 lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w"
@@ -58,14 +58,6 @@
   "False \<Longrightarrow> number_of x = number_of y"
   by (rule FalseE)
 
-lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE]
-
-lemma BIT_eq_iff [simp]: 
-  "(u BIT b = v BIT c) = (u = v \<and> b = c)"
-  by (rule iffI) auto
-
-lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]
-
 lemma less_Bits: 
   "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
   unfolding Bit_def by (auto simp add: bitval_def split: bit.split)
@@ -249,7 +241,7 @@
   apply (erule allE)
   apply (erule impE)
    prefer 2
-   apply (erule BIT_eqI)
+   apply (erule conjI)
    apply (drule_tac x=0 in fun_cong, force)
   apply (rule ext)
   apply (drule_tac x="Suc ?x" in fun_cong, force)