diff --git a/thys/Native_Word/Code_Target_Int_Bit.thy b/thys/Native_Word/Code_Target_Int_Bit.thy
--- a/thys/Native_Word/Code_Target_Int_Bit.thy
+++ b/thys/Native_Word/Code_Target_Int_Bit.thy
@@ -1,100 +1,65 @@
 (*  Title:      Code_Target_Int_Bit.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Implementation of bit operations on int by target language operations\<close>
 
 theory Code_Target_Int_Bit
   imports
   Code_Target_Integer_Bit
   "HOL-Library.Code_Target_Int"
 begin
 
 context
   includes bit_operations_syntax
 begin
 
 declare [[code drop:
-  "(AND) :: int \<Rightarrow> _" "(OR) :: int \<Rightarrow> _" "(XOR) :: int \<Rightarrow> _" "NOT :: int \<Rightarrow> _"
-  "lsb :: int \<Rightarrow> _" "set_bit :: int \<Rightarrow> _" "bit :: int \<Rightarrow> _"
-  "push_bit :: _ \<Rightarrow> int \<Rightarrow> _" "drop_bit :: _ \<Rightarrow> int \<Rightarrow> _"
-  int_of_integer_symbolic
+  "lsb :: int \<Rightarrow> _" int_of_integer_symbolic
   ]]
 
 lemma [code_unfold]:
   \<open>of_bool (odd i) = i AND 1\<close> for i :: int
   by (simp add: and_one_eq mod2_eq_if)
 
 lemma [code_unfold]:
   \<open>bit x n \<longleftrightarrow> x AND (push_bit n 1) \<noteq> 0\<close> for x :: int
   by (fact bit_iff_and_push_bit_not_eq_0)
 
 context
 includes integer.lifting
 begin
 
-lemma bit_int_code [code]:
-  "bit (int_of_integer x) n = bit x n"
-  by transfer simp
-
-lemma and_int_code [code]:
-  "int_of_integer i AND int_of_integer j = int_of_integer (i AND j)"
-  by transfer simp
-
-lemma or_int_code [code]:
-  "int_of_integer i OR int_of_integer j = int_of_integer (i OR j)"
-  by transfer simp
-
-lemma xor_int_code [code]:
-  "int_of_integer i XOR int_of_integer j = int_of_integer (i XOR j)"
-  by transfer simp
-
-lemma not_int_code [code]:
-  "NOT (int_of_integer i) = int_of_integer (NOT i)"
-  by transfer simp
-
-lemma push_bit_int_code [code]:
-  \<open>push_bit n (int_of_integer x) = int_of_integer (push_bit n x)\<close>
-  by transfer simp
-
-lemma drop_bit_int_code [code]:
-  \<open>drop_bit n (int_of_integer x) = int_of_integer (drop_bit n x)\<close>
-  by transfer simp
-
-lemma take_bit_int_code [code]:
-  \<open>take_bit n (int_of_integer x) = int_of_integer (take_bit n x)\<close>
-  by transfer simp
-
 lemma lsb_int_code [code]:
   "lsb (int_of_integer x) = lsb x"
   by transfer simp
 
 lemma set_bit_int_code [code]:
   "set_bit (int_of_integer x) n b = int_of_integer (set_bit x n b)"
   by transfer simp
 
 lemma int_of_integer_symbolic_code [code]:
   "int_of_integer_symbolic = int_of_integer"
   by (simp add: int_of_integer_symbolic_def)
 
 context
 begin
 
 qualified definition even :: \<open>int \<Rightarrow> bool\<close>
   where [code_abbrev]: \<open>even = Parity.even\<close>
 
 end
 
 lemma [code]:
   \<open>Code_Target_Int_Bit.even i \<longleftrightarrow> i AND 1 = 0\<close>
   by (simp add: Code_Target_Int_Bit.even_def even_iff_mod_2_eq_zero and_one_eq)
 
 lemma bin_rest_code:
   "int_of_integer i div 2 = int_of_integer (bin_rest_integer i)"
   by transfer simp
 
 end
 
 end
 
 end
diff --git a/thys/Word_Lib/Bit_Comprehension.thy b/thys/Word_Lib/Bit_Comprehension.thy
--- a/thys/Word_Lib/Bit_Comprehension.thy
+++ b/thys/Word_Lib/Bit_Comprehension.thy
@@ -1,88 +1,88 @@
 (*
  * Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section \<open>Comprehension syntax for bit expressions\<close>
 
 theory Bit_Comprehension
   imports
     "HOL-Library.Word"
 begin
 
 class bit_comprehension = ring_bit_operations +
   fixes set_bits :: \<open>(nat \<Rightarrow> bool) \<Rightarrow> 'a\<close>  (binder \<open>BITS \<close> 10)
   assumes set_bits_bit_eq: \<open>set_bits (bit a) = a\<close>
 begin
 
 lemma set_bits_False_eq [simp]:
   \<open>(BITS _. False) = 0\<close>
   using set_bits_bit_eq [of 0] by (simp add: bot_fun_def)
 
 end
 
 instantiation word :: (len) bit_comprehension
 begin
 
 definition word_set_bits_def:
   \<open>(BITS n. P n) = (horner_sum of_bool 2 (map P [0..<LENGTH('a)]) :: 'a word)\<close>
 
 instance by standard
   (simp add: word_set_bits_def horner_sum_bit_eq_take_bit)
 
 end
 
 lemma bit_set_bits_word_iff [bit_simps]:
   \<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close>
   by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)
 
 lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. bit i n)"
   by (rule bit_eqI) (auto simp add: bit_simps)
 
-lemma set_bits_K_False [simp]:
+lemma set_bits_K_False:
   \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close>
-  by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff)
+  by (fact set_bits_False_eq)
 
 lemma word_test_bit_set_bits: "bit (BITS n. f n :: 'a :: len word) n \<longleftrightarrow> n < LENGTH('a) \<and> f n"
   by (fact bit_set_bits_word_iff)
 
 context
   includes bit_operations_syntax
   fixes f :: \<open>nat \<Rightarrow> bool\<close>
 begin
 
 definition set_bits_aux :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a::len word\<close>
   where \<open>set_bits_aux n w = push_bit n w OR take_bit n (set_bits f)\<close>
 
 lemma bit_set_bit_aux [bit_simps]:
   \<open>bit (set_bits_aux n w) m \<longleftrightarrow> m < LENGTH('a) \<and>
     (if m < n then f m else bit w (m - n))\<close> for w :: \<open>'a::len word\<close>
   by (auto simp add: bit_simps set_bits_aux_def)
 
 corollary set_bits_conv_set_bits_aux:
   \<open>set_bits f = (set_bits_aux LENGTH('a) 0 :: 'a :: len word)\<close>
   by (rule bit_word_eqI) (simp add: bit_simps)
 
 lemma set_bits_aux_0 [simp]:
   \<open>set_bits_aux 0 w = w\<close>
   by (simp add: set_bits_aux_def)
 
 lemma set_bits_aux_Suc [simp]:
   \<open>set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\<close>
   by (rule bit_word_eqI) (auto simp add: bit_simps le_less_Suc_eq mult.commute [of _ 2])
 
 lemma set_bits_aux_simps [code]:
   \<open>set_bits_aux 0 w = w\<close>
   \<open>set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\<close>
   by simp_all
 
 lemma set_bits_aux_rec:
   \<open>set_bits_aux n w =
   (if n = 0 then w
    else let n' = n - 1 in set_bits_aux n' (push_bit 1 w OR (if f n' then 1 else 0)))\<close>
   by (cases n) simp_all
 
 end
 
 end