src/HOL/Int.thy

--- a/src/HOL/Int.thy	Wed Jul 29 09:06:49 2009 +0200
+++ b/src/HOL/Int.thy	Wed Jul 29 16:42:47 2009 +0200
@@ -1000,11 +1000,11 @@
   Converting numerals 0 and 1 to their abstract versions.
 *}
 
-lemma numeral_0_eq_0 [simp]:
+lemma numeral_0_eq_0 [simp, code_post]:
   "Numeral0 = (0::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp
 
-lemma numeral_1_eq_1 [simp]:
+lemma numeral_1_eq_1 [simp, code_post]:
   "Numeral1 = (1::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp