added numeral code postprocessor rules on type int
authorhaftmann
Wed Jul 29 16:42:47 2009 +0200 (2009-07-29)
changeset 32272cc1bf9077167
parent 32269 b642e4813e53
child 32273 3c395fc7ec5e
added numeral code postprocessor rules on type int
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Wed Jul 29 09:06:49 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Wed Jul 29 16:42:47 2009 +0200
     1.3 @@ -1000,11 +1000,11 @@
     1.4    Converting numerals 0 and 1 to their abstract versions.
     1.5  *}
     1.6  
     1.7 -lemma numeral_0_eq_0 [simp]:
     1.8 +lemma numeral_0_eq_0 [simp, code_post]:
     1.9    "Numeral0 = (0::'a::number_ring)"
    1.10    unfolding number_of_eq numeral_simps by simp
    1.11  
    1.12 -lemma numeral_1_eq_1 [simp]:
    1.13 +lemma numeral_1_eq_1 [simp, code_post]:
    1.14    "Numeral1 = (1::'a::number_ring)"
    1.15    unfolding number_of_eq numeral_simps by simp
    1.16