--- a/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 16:27:34 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Jul 15 10:11:13 2009 +0200
@@ -320,9 +320,7 @@
returns @{text "0"}.
*}
-definition
- int :: "nat \<Rightarrow> int"
-where
+definition int :: "nat \<Rightarrow> int" where
[code del]: "int = of_nat"
lemma int_code' [code]:
@@ -336,6 +334,10 @@
lemma of_nat_int [code_unfold_post]:
"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)
+
code_const int
(SML "_")
(OCaml "_")