author | haftmann |
Wed, 29 Jul 2009 16:42:47 +0200 | |
changeset 32272 | cc1bf9077167 |
parent 32269 | b642e4813e53 |
child 32273 | 3c395fc7ec5e |
src/HOL/Int.thy | file | annotate | diff | comparison | revisions |
--- 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