src/HOL/Library/Code_Target_Int.thy
changeset 54891 2f4491f15fe6
parent 54796 cdc6d8cbf770
child 55736 f1ed1e9cd080
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Wed Jan 01 01:05:48 2014 +0100
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Wed Jan 01 11:35:21 2014 +0100
     1.3 @@ -10,8 +10,7 @@
     1.4  
     1.5  code_datatype int_of_integer
     1.6  
     1.7 -lemma [code, code del]:
     1.8 -  "integer_of_int = integer_of_int" ..
     1.9 +declare [[code drop: integer_of_int]]
    1.10  
    1.11  lemma [code]:
    1.12    "integer_of_int (int_of_integer k) = k"
    1.13 @@ -57,8 +56,7 @@
    1.14    "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
    1.15    by transfer simp
    1.16  
    1.17 -lemma [code, code del]:
    1.18 -  "Int.sub = Int.sub" ..
    1.19 +declare [[code drop: Int.sub]]
    1.20  
    1.21  lemma [code]:
    1.22    "k * l = int_of_integer (of_int k * of_int l)"