--- 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