changeset 72082 | 41393ecb57ac |
parent 71988 | ace45a11a45e |
child 73535 | 0f33c7031ec9 |
--- a/src/HOL/Library/Z2.thy Tue Aug 04 09:24:00 2020 +0000 +++ b/src/HOL/Library/Z2.thy Tue Aug 04 09:33:05 2020 +0000 @@ -187,6 +187,9 @@ definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> where [simp]: \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit +definition mask_bit :: \<open>nat \<Rightarrow> bit\<close> + where [simp]: \<open>mask_bit n = of_bool (n > 0)\<close> + instance by standard auto