src/HOL/Library/Nat_Bijection.thy
changeset 39302 d7728f65b353
parent 37591 d3daea901123
child 41959 b460124855b8
     1.1 --- a/src/HOL/Library/Nat_Bijection.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -333,8 +333,8 @@
     1.4  lemma set_decode_plus_power_2:
     1.5    "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
     1.6   apply (induct n arbitrary: z, simp_all)
     1.7 -  apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2)
     1.8 - apply (rule set_ext, induct_tac x, simp, simp add: add_commute)
     1.9 +  apply (rule set_eqI, induct_tac x, simp, simp add: even_nat_Suc_div_2)
    1.10 + apply (rule set_eqI, induct_tac x, simp, simp add: add_commute)
    1.11  done
    1.12  
    1.13  lemma finite_set_decode [simp]: "finite (set_decode n)"