1.1 --- a/src/HOL/Code_Numeral.thy	Thu Dec 29 10:47:55 2011 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Dec 29 10:47:55 2011 +0100
     1.3 @@ -176,16 +176,18 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma zero_code_numeral_code [code, code_unfold]:
     1.8 +lemma zero_code_numeral_code [code]:
     1.9    "(0\<Colon>code_numeral) = Numeral0"
    1.10    by (simp add: number_of_code_numeral_def Pls_def)
    1.11 -lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
    1.12 +
    1.13 +lemma [code_abbrev]: "Numeral0 = (0\<Colon>code_numeral)"
    1.14    using zero_code_numeral_code ..
    1.15  
    1.16 -lemma one_code_numeral_code [code, code_unfold]:
    1.17 +lemma one_code_numeral_code [code]:
    1.18    "(1\<Colon>code_numeral) = Numeral1"
    1.19    by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
    1.20 -lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
    1.21 +
    1.22 +lemma [code_abbrev]: "Numeral1 = (1\<Colon>code_numeral)"
    1.23    using one_code_numeral_code ..
    1.24  
    1.25  lemma plus_code_numeral_code [code nbe]: