src/HOL/Library/Target_Numeral.thy

--- a/src/HOL/Library/Target_Numeral.thy	Sat Apr 28 18:09:50 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy	Sun Apr 29 09:25:54 2012 +0200
@@ -632,6 +632,10 @@
 
 hide_const (open) of_nat Nat
 
+lemma [code_unfold]:
+  "Int.nat (Target_Numeral.int_of k) = Target_Numeral.nat_of k"
+  by (simp add: nat_of_def)
+
 lemma int_of_nat [simp]:
   "Target_Numeral.int_of (Target_Numeral.of_nat n) = of_nat n"
   by (simp add: of_nat_def)