--- 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"
--- 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])