--- a/src/HOL/Library/Z2.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/Library/Z2.thy Sun Aug 01 10:20:34 2021 +0000
@@ -178,6 +178,10 @@
instantiation bit :: semiring_bit_operations
begin
+context
+ includes bit_operations_syntax
+begin
+
definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
where [simp]: \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit
@@ -199,17 +203,19 @@
definition flip_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
where [simp]: \<open>flip_bit n b = of_bool ((n = 0) \<noteq> odd b)\<close> for b :: bit
+end
+
instance
by standard auto
end
lemma add_bit_eq_xor [simp, code]:
- \<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close>
+ \<open>(+) = (Bit_Operations.xor :: bit \<Rightarrow> _)\<close>
by (auto simp add: fun_eq_iff)
lemma mult_bit_eq_and [simp, code]:
- \<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close>
+ \<open>(*) = (Bit_Operations.and :: bit \<Rightarrow> _)\<close>
by (simp add: fun_eq_iff)
instantiation bit :: field