changeset 71921 | a238074c5a9d |
parent 71823 | 214b48a1937b |
child 71922 | 2c6a5c709f22 |
--- a/src/HOL/ex/Bit_Operations.thy Thu Jun 04 15:30:22 2020 +0000 +++ b/src/HOL/ex/Bit_Operations.thy Thu Jun 04 19:38:50 2020 +0000 @@ -57,11 +57,11 @@ "a AND 0 = 0" by (simp add: bit_eq_iff bit_and_iff) -lemma one_and_eq [simp]: +lemma one_and_eq: "1 AND a = a mod 2" by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff) -lemma and_one_eq [simp]: +lemma and_one_eq: "a AND 1 = a mod 2" using one_and_eq [of a] by (simp add: ac_simps)