1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 16:27:31 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 16:27:32 2009 +0200
     1.3 @@ -26,15 +26,13 @@
     1.4  
     1.5  code_datatype number_nat_inst.number_of_nat
     1.6  
     1.7 -lemma zero_nat_code [code, code_inline]:
     1.8 +lemma zero_nat_code [code, code_unfold_post]:
     1.9    "0 = (Numeral0 :: nat)"
    1.10    by simp
    1.11 -lemmas [code_post] = zero_nat_code [symmetric]
    1.12  
    1.13 -lemma one_nat_code [code, code_inline]:
    1.14 +lemma one_nat_code [code, code_unfold_post]:
    1.15    "1 = (Numeral1 :: nat)"
    1.16    by simp
    1.17 -lemmas [code_post] = one_nat_code [symmetric]
    1.18  
    1.19  lemma Suc_code [code]:
    1.20    "Suc n = n + 1"
    1.21 @@ -302,7 +300,7 @@
    1.22    Natural numerals.
    1.23  *}
    1.24  
    1.25 -lemma [code_inline, symmetric, code_post]:
    1.26 +lemma [code_unfold_post]:
    1.27    "nat (number_of i) = number_nat_inst.number_of_nat i"
    1.28    -- {* this interacts as desired with @{thm nat_number_of_def} *}
    1.29    by (simp add: number_nat_inst.number_of_nat)
    1.30 @@ -335,9 +333,8 @@
    1.31    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
    1.32    unfolding nat_number_of_def number_of_is_id neg_def by simp
    1.33  
    1.34 -lemma of_nat_int [code_unfold]:
    1.35 +lemma of_nat_int [code_unfold_post]:
    1.36    "of_nat = int" by (simp add: int_def)
    1.37 -declare of_nat_int [symmetric, code_post]
    1.38  
    1.39  code_const int
    1.40    (SML "_")