1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -26,15 +26,15 @@
     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_inline]:
     1.9    "0 = (Numeral0 :: nat)"
    1.10    by simp
    1.11 -lemmas [code post] = zero_nat_code [symmetric]
    1.12 +lemmas [code_post] = zero_nat_code [symmetric]
    1.13  
    1.14 -lemma one_nat_code [code, code inline]:
    1.15 +lemma one_nat_code [code, code_inline]:
    1.16    "1 = (Numeral1 :: nat)"
    1.17    by simp
    1.18 -lemmas [code post] = one_nat_code [symmetric]
    1.19 +lemmas [code_post] = one_nat_code [symmetric]
    1.20  
    1.21  lemma Suc_code [code]:
    1.22    "Suc n = n + 1"
    1.23 @@ -89,7 +89,7 @@
    1.24    expression:
    1.25  *}
    1.26  
    1.27 -lemma [code, code unfold]:
    1.28 +lemma [code, code_unfold]:
    1.29    "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    1.30    by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
    1.31  
    1.32 @@ -302,7 +302,7 @@
    1.33    Natural numerals.
    1.34  *}
    1.35  
    1.36 -lemma [code inline, symmetric, code post]:
    1.37 +lemma [code_inline, symmetric, code_post]:
    1.38    "nat (number_of i) = number_nat_inst.number_of_nat i"
    1.39    -- {* this interacts as desired with @{thm nat_number_of_def} *}
    1.40    by (simp add: number_nat_inst.number_of_nat)
    1.41 @@ -335,9 +335,9 @@
    1.42    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
    1.43    unfolding nat_number_of_def number_of_is_id neg_def by simp
    1.44  
    1.45 -lemma of_nat_int [code unfold]:
    1.46 +lemma of_nat_int [code_unfold]:
    1.47    "of_nat = int" by (simp add: int_def)
    1.48 -declare of_nat_int [symmetric, code post]
    1.49 +declare of_nat_int [symmetric, code_post]
    1.50  
    1.51  code_const int
    1.52    (SML "_")