src/HOL/Library/Code_Target_Int.thy

--- a/src/HOL/Library/Code_Target_Int.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -10,8 +10,6 @@
 
 code_datatype int_of_integer
 
-declare [[code drop: integer_of_int]]
-
 context
 includes integer.lifting
 begin
@@ -112,8 +110,6 @@
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
 
-declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
-
 lemma gcd_int_of_integer [code]:
   "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
   by transfer rule
@@ -163,10 +159,6 @@
   includes integer.lifting and bit_operations_syntax
 begin
 
-declare [[code drop: \<open>bit :: int \<Rightarrow> _\<close> \<open>not :: int \<Rightarrow> _\<close>
-  \<open>and :: int \<Rightarrow> _\<close> \<open>or :: int \<Rightarrow> _\<close> \<open>xor :: int \<Rightarrow> _\<close>
-  \<open>push_bit :: _ \<Rightarrow> _ \<Rightarrow> int\<close> \<open>drop_bit :: _ \<Rightarrow> _ \<Rightarrow> int\<close> \<open>take_bit :: _ \<Rightarrow> _ \<Rightarrow> int\<close>]]
-
 lemma [code]:
   \<open>bit (int_of_integer k) n \<longleftrightarrow> bit k n\<close>
   by transfer rule