# HG changeset patch
# User wenzelm
# Date 1474225584 -7200
# Node ID 5e816da75b8f87731ba40c18fc5cf1eb3f49192c
# Parent  255294779d401332a9ee55df0c09d1a4692a82e7# Parent  bab633745c7fd4dbf6eafc66a3d886f5c1618735
merged

diff -r bab633745c7f -r 5e816da75b8f src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sun Sep 18 20:33:48 2016 +0200
+++ b/src/HOL/Num.thy	Sun Sep 18 21:06:24 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"
diff -r bab633745c7f -r 5e816da75b8f src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Sun Sep 18 20:33:48 2016 +0200
+++ b/src/HOL/ex/Primrec.thy	Sun Sep 18 21:06:24 2016 +0200
@@ -129,7 +129,7 @@
 text \<open>PROPERTY A 10\<close>
 
 lemma ack_nest_bound: "ack i1 (ack i2 j) < ack (2 + (i1 + i2)) j"
-apply (simp add: numerals)
+apply simp
 apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
 apply simp
 apply (rule le_add1 [THEN ack_le_mono1, THEN le_less_trans])