src/HOL/Num.thy

--- a/src/HOL/Num.thy	Sun Sep 18 11:31:19 2016 +0200
+++ b/src/HOL/Num.thy	Sun Sep 18 18:23:59 2016 +0200
@@ -994,6 +994,8 @@
 lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)"
   by (rule numeral_One) (rule numeral_2_eq_2)
 
+lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def
+
 text \<open>Comparisons involving @{term Suc}.\<close>
 
 lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"