--- a/src/HOL/Bit_Operations.thy Wed Aug 17 20:37:16 2022 +0000
+++ b/src/HOL/Bit_Operations.thy Fri Aug 19 05:49:06 2022 +0000
@@ -7,15 +7,6 @@
imports Presburger Groups_List
begin
-lemma half_nonnegative_int_iff [simp]:
- \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
- by auto
-
-lemma half_negative_int_iff [simp]:
- \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
- by auto
-
-
subsection \<open>Abstract bit structures\<close>
class semiring_bits = semiring_parity +