# HG changeset patch
# User haftmann
# Date 1624514792 0
# Node ID f46e9f75b7d5bb117bded29c3c27634066008da2
# Parent  d156b141fe2f8ad64ef6f10578e59627b0275078
more word cleanup

diff -r d156b141fe2f -r f46e9f75b7d5 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Wed Jun 23 18:38:37 2021 +0000
+++ b/src/HOL/Library/Bit_Operations.thy	Thu Jun 24 06:06:32 2021 +0000
@@ -9,11 +9,6 @@
     "HOL-Library.Boolean_Algebra"
 begin
 
-lemma bit_numeral_int_iff [bit_simps]: \<comment> \<open>TODO: move\<close>
-  \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
-  using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
-
-
 subsection \<open>Bit operations\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
diff -r d156b141fe2f -r f46e9f75b7d5 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Jun 23 18:38:37 2021 +0000
+++ b/src/HOL/Parity.thy	Thu Jun 24 06:06:32 2021 +0000
@@ -1818,6 +1818,10 @@
 
 instance int :: unique_euclidean_semiring_with_bit_shifts ..
 
+lemma bit_numeral_int_iff [bit_simps]:
+  \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
+  using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
+
 lemma bit_not_int_iff':
   \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
   for k :: int