more word cleanup
authorhaftmann
Thu, 24 Jun 2021 06:06:32 +0000
changeset 74131 f46e9f75b7d5
parent 74130 d156b141fe2f
child 74132 ced6e3c03425
more word cleanup
src/HOL/Library/Bit_Operations.thy
src/HOL/Parity.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 +
--- 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