# HG changeset patch
# User haftmann
# Date 1248878567 -7200
# Node ID cc1bf9077167d4faca10c8c3c2401f22bcb8ab3a
# Parent  b642e4813e538fe3adbcbfc4dd593a481307d5b7
added numeral code postprocessor rules on type int

diff -r b642e4813e53 -r cc1bf9077167 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