# HG changeset patch
# User haftmann
# Date 1335684354 -7200
# Node ID 4ad2b7ccd0ff8184efaa82c43479090cbb630748
# Parent  0e36cc70cb3ed3a1049c57abeaf571be18b6c7cd
compact nat literals

diff -r 0e36cc70cb3e -r 4ad2b7ccd0ff 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)