convenient printing of (- 1 :: integer) after code evaluation
authorhaftmann
Sun Aug 31 09:10:40 2014 +0200 (2014-08-31)
changeset 580997f232ae7de7c
parent 58098 ff478d85129b
child 58100 f54a8a4134d3
convenient printing of (- 1 :: integer) after code evaluation
src/HOL/Library/Code_Target_Int.thy
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Sat Aug 30 11:15:47 2014 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sun Aug 31 09:10:40 2014 +0200
     1.3 @@ -44,6 +44,10 @@
     1.4    "1 = int_of_integer 1"
     1.5    by transfer simp
     1.6  
     1.7 +lemma [code_post]:
     1.8 +  "int_of_integer (- 1) = - 1"
     1.9 +  by simp
    1.10 +
    1.11  lemma [code]:
    1.12    "k + l = int_of_integer (of_int k + of_int l)"
    1.13    by transfer simp