diff -r b90bf6636260 -r 7476818dfd5d src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sat Dec 02 20:49:48 2023 +0000
+++ b/src/HOL/Bit_Operations.thy	Sat Dec 02 20:49:49 2023 +0000
@@ -5,7 +5,7 @@
 
 theory Bit_Operations
   imports Presburger Groups_List
-begin
+begin                 
 
 subsection \<open>Abstract bit structures\<close>
 
@@ -83,10 +83,6 @@
   \<open>0 mod a = 0\<close>
   using div_mult_mod_eq [of 0 a] by simp
 
-lemma bits_one_mod_two_eq_one [simp]:
-  \<open>1 mod 2 = 1\<close>
-  by (simp add: mod2_eq_if)
-
 lemma bit_0:
   \<open>bit a 0 \<longleftrightarrow> odd a\<close>
   by (simp add: bit_iff_odd)
@@ -3764,6 +3760,8 @@
 context semiring_bit_operations
 begin
 
+lemmas bits_one_mod_two_eq_one [no_atp] = one_mod_two_eq_one
+
 lemmas set_bit_def [no_atp] = set_bit_eq_or
 
 lemmas unset_bit_def [no_atp] = unset_bit_eq_and_not