tuned code postprocessor
authorhaftmann
Fri May 15 16:39:18 2009 +0200 (2009-05-15)
changeset 311827ac0a57a57ed
parent 31181 27304e12a412
child 31183 13effe47174c
tuned code postprocessor
src/HOL/Nat_Numeral.thy
     1.1 --- a/src/HOL/Nat_Numeral.thy	Fri May 15 16:39:17 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Fri May 15 16:39:18 2009 +0200
     1.3 @@ -316,13 +316,13 @@
     1.4  lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
     1.5  by (simp add: nat_number_of_def)
     1.6  
     1.7 -lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
     1.8 +lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
     1.9  by (simp add: nat_number_of_def)
    1.10  
    1.11  lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
    1.12  by (simp add: nat_1 nat_number_of_def)
    1.13  
    1.14 -lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    1.15 +lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
    1.16  by (simp add: nat_numeral_1_eq_1)
    1.17  
    1.18