tuned
authornipkow
Wed Dec 06 09:11:27 2017 +0100 (7 months ago)
changeset 67142fa1173288322
parent 67141 94fca35f80ab
child 67143 db609ac2c307
child 67145 e77c5bfca9aa
tuned
src/HOL/Word/Bit_Representation.thy
     1.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 05 16:54:37 2017 +0100
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 06 09:11:27 2017 +0100
     1.3 @@ -139,14 +139,8 @@
     1.4  lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
     1.5    by (metis bin_rl_simp)
     1.6  
     1.7 -lemma bin_exhaust:
     1.8 -  assumes that: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
     1.9 -  shows "Q"
    1.10 -  apply (insert bin_ex_rl [of bin])
    1.11 -  apply (erule exE)+
    1.12 -  apply (rule that)
    1.13 -  apply force
    1.14 -  done
    1.15 +lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
    1.16 +by (metis bin_ex_rl)
    1.17  
    1.18  primrec bin_nth
    1.19    where