src/HOL/Library/Code_Target_Int.thy
changeset 58099 7f232ae7de7c
parent 57512 cc97b347b301
child 58881 b9556a055632
     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