# 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