--- a/src/HOL/Nat_Numeral.thy Fri May 15 16:39:17 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Fri May 15 16:39:18 2009 +0200
@@ -316,13 +316,13 @@
lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
by (simp add: nat_number_of_def)
-lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
+lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
by (simp add: nat_number_of_def)
lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
by (simp add: nat_1 nat_number_of_def)
-lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
+lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
by (simp add: nat_numeral_1_eq_1)