# HG changeset patch
# User haftmann
# Date 1196258959 -3600
# Node ID c945521fa0d9a7a0ce8b1531806226f07bf9e950
# Parent  d96d5808d92673dee45d654c59730eacf14238ef
deleted looping code theorem

diff -r d96d5808d926 -r c945521fa0d9 src/HOL/Library/Efficient_Nat.thy
--- 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"