| changeset 71755 | 318695613bb7 |
| parent 71535 | b612edee9b0c |
| child 71757 | 02c50bba9304 |
--- a/src/HOL/Parity.thy Thu Apr 16 00:37:07 2020 +0200 +++ b/src/HOL/Parity.thy Thu Apr 16 08:09:28 2020 +0200 @@ -152,6 +152,10 @@ then show False by simp qed +lemma odd_numeral_BitM [simp]: + \<open>odd (numeral (Num.BitM w))\<close> + by (cases w) simp_all + lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" by (induct n) auto