convenient printing of (- 1 :: integer) after code evaluation
authorhaftmann
Sun, 31 Aug 2014 09:10:40 +0200
changeset 58099 7f232ae7de7c
parent 58098 ff478d85129b
child 58100 f54a8a4134d3
convenient printing of (- 1 :: integer) after code evaluation
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