src/HOL/Library/Efficient_Nat.thy

   using their counterparts on the integers:
 *}
 
 code_datatype number_nat_inst.number_of_nat
 
-lemma zero_nat_code [code, code_unfold_post]:
+lemma zero_nat_code [code, code_unfold]:
   "0 = (Numeral0 :: nat)"
   by simp
 
-lemma one_nat_code [code, code_unfold_post]:
+lemma one_nat_code [code, code_unfold]:
   "1 = (Numeral1 :: nat)"
   by simp
 
 lemma Suc_code [code]:
   "Suc n = n + 1"

 
 text {*
   Natural numerals.
 *}
 
-lemma [code_unfold_post]:
-  "nat (number_of i) = number_nat_inst.number_of_nat i"
+lemma [code_abbrev]:
+  "number_nat_inst.number_of_nat i = nat (number_of i)"
   -- {* this interacts as desired with @{thm nat_number_of_def} *}
   by (simp add: number_nat_inst.number_of_nat)
 
 setup {*
   fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}

   returns its input value, provided that it is non-negative, and otherwise
   returns @{text "0"}.
 *}
 
 definition int :: "nat \<Rightarrow> int" where
-  [code del]: "int = of_nat"
+  [code del, code_abbrev]: "int = of_nat"
 
 lemma int_code' [code]:
   "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   unfolding int_nat_number_of [folded int_def] ..
 
 lemma nat_code' [code]:
   "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   unfolding nat_number_of_def number_of_is_id neg_def by simp
 
-lemma of_nat_int [code_unfold_post]:
+lemma of_nat_int: (* FIXME delete candidate *)
   "of_nat = int" by (simp add: int_def)
 
 lemma of_nat_aux_int [code_unfold]:
   "of_nat_aux (\<lambda>i. i + 1) k 0 = int k"
   by (simp add: int_def Nat.of_nat_code)