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