# HG changeset patch
# User haftmann
# Date 1360913490 -3600
# Node ID ac9e909fe55d9d5e8000de8dd08dcf81eae3c2f9
# Parent  cc7423ce677414aee2043166012450013fb64917
explicit code equation for integer_of_nat

diff -r cc7423ce6774 -r ac9e909fe55d src/HOL/Library/Code_Numeral_Types.thy
--- a/src/HOL/Library/Code_Numeral_Types.thy	Fri Feb 15 11:31:59 2013 +0100
+++ b/src/HOL/Library/Code_Numeral_Types.thy	Fri Feb 15 08:31:30 2013 +0100
@@ -111,6 +111,10 @@
   is "of_nat :: nat \<Rightarrow> int"
   .
 
+lemma integer_of_nat_eq_of_nat [code]:
+  "integer_of_nat = of_nat"
+  by transfer rule
+
 lemma int_of_integer_integer_of_nat [simp]:
   "int_of_integer (integer_of_nat n) = of_nat n"
   by transfer rule