# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1474215839 -7200
# Node ID 6b886cadba7cfed078fe58e2910415366cf389b3
# Parent  ca41b6670904e62b90f5d196069db8d7cbfe74c6
tuned

diff -r ca41b6670904 -r 6b886cadba7c 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"
diff -r ca41b6670904 -r 6b886cadba7c src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Sun Sep 18 11:31:19 2016 +0200
+++ b/src/HOL/ex/Primrec.thy	Sun Sep 18 18:23:59 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])