| changeset 25488 | c945521fa0d9 |
| parent 24994 | c385c4eabb3b |
| child 25615 | b337edd55a07 |
--- a/src/HOL/Library/Efficient_Nat.thy Wed Nov 28 14:56:38 2007 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Wed Nov 28 15:09:19 2007 +0100 @@ -33,7 +33,7 @@ definition int_of_nat :: "nat \<Rightarrow> int" where - "int_of_nat n = of_nat n" + [code func del]: "int_of_nat n = of_nat n" lemma int_of_nat_Suc [simp]: "int_of_nat (Suc n) = 1 + int_of_nat n"