# HG changeset patch
# User haftmann
# Date 1409469040 -7200
# Node ID 7f232ae7de7cb148eb3c1940674c75d7abf37a82
# Parent  ff478d85129b2cf7228abc1fbfa152fcc9275ddf
convenient printing of (- 1 :: integer) after code evaluation

diff -r ff478d85129b -r 7f232ae7de7c src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Sat Aug 30 11:15:47 2014 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Sun Aug 31 09:10:40 2014 +0200
@@ -44,6 +44,10 @@
   "1 = int_of_integer 1"
   by transfer simp
 
+lemma [code_post]:
+  "int_of_integer (- 1) = - 1"
+  by simp
+
 lemma [code]:
   "k + l = int_of_integer (of_int k + of_int l)"
   by transfer simp