# HG changeset patch
# User haftmann
# Date 1587017368 -7200
# Node ID 318695613bb7010468b18ccd120509bbf9b1ff60
# Parent  2006be3cb98b7e1d8873eca470b00d2318042523
more complete rules on numerals

diff -r 2006be3cb98b -r 318695613bb7 src/HOL/Parity.thy
--- 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