additional preprocessor rule
authorhaftmann
Wed Jul 15 10:11:13 2009 +0200 (2009-07-15)
changeset 320730a83608e21f1
parent 32072 d4bff63bcbf1
child 32074 76d6ba08a05f
child 32076 05d915945bc6
additional preprocessor rule
src/HOL/Library/Efficient_Nat.thy
     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 "_")