src/HOL/Word/Bit_Comprehension.thy

   show \<open>set_bits (bit k) = k\<close>
     apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l)
     apply simp
     apply (rule bit_eqI)
     apply (simp add: bit_signed_take_bit_iff min_def)
-    using "*" by blast
+    apply (auto simp add: not_le bit_take_bit_iff dest: *)
+    done
 qed
 
 end
 
 lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)"

       done
   qed
 qed
 
 lemma bin_last_set_bits [simp]:
-  "bin_last (set_bits f) = f 0"
+  "odd (set_bits f :: int) = f 0"
   by (subst int_set_bits_unfold_BIT) simp_all
 
 lemma bin_rest_set_bits [simp]:
-  "bin_rest (set_bits f) = set_bits (f \<circ> Suc)"
+  "set_bits f div (2 :: int) = set_bits (f \<circ> Suc)"
   by (subst int_set_bits_unfold_BIT) simp_all
 
 lemma bin_nth_set_bits [simp]:
-  "bin_nth (set_bits f) m = f m"
+  "bit (set_bits f :: int) m \<longleftrightarrow> f m"
 using wff proof (induction m arbitrary: f)
   case 0 
   then show ?case
     by (simp add: Bit_Comprehension.bin_last_set_bits)
 next