--- a/src/HOL/Word/Bit_Representation.thy Tue Dec 05 16:54:37 2017 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Wed Dec 06 09:11:27 2017 +0100
@@ -139,14 +139,8 @@
lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
by (metis bin_rl_simp)
-lemma bin_exhaust:
- assumes that: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
- shows "Q"
- apply (insert bin_ex_rl [of bin])
- apply (erule exE)+
- apply (rule that)
- apply force
- done
+lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
+by (metis bin_ex_rl)
primrec bin_nth
where