src/HOL/Library/Efficient_Nat.thy
changeset 32073 0a83608e21f1
parent 32069 6d28bbd33e2c
child 32348 36dbff4841ab
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 16:27:34 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jul 15 10:11:13 2009 +0200
     1.3 @@ -320,9 +320,7 @@
     1.4    returns @{text "0"}.
     1.5  *}
     1.6  
     1.7 -definition
     1.8 -  int :: "nat \<Rightarrow> int"
     1.9 -where
    1.10 +definition int :: "nat \<Rightarrow> int" where
    1.11    [code del]: "int = of_nat"
    1.12  
    1.13  lemma int_code' [code]:
    1.14 @@ -336,6 +334,10 @@
    1.15  lemma of_nat_int [code_unfold_post]:
    1.16    "of_nat = int" by (simp add: int_def)
    1.17  
    1.18 +lemma of_nat_aux_int [code_unfold]:
    1.19 +  "of_nat_aux (\<lambda>i. i + 1) k 0 = int k"
    1.20 +  by (simp add: int_def Nat.of_nat_code)
    1.21 +
    1.22  code_const int
    1.23    (SML "_")
    1.24    (OCaml "_")