# HG changeset patch # User haftmann # Date 1388572521 -3600 # Node ID 2f4491f15fe6ed03cb9354862fd1b401cd2840ce # Parent cb892d835803436bf88dd8003260e0339bdbbb51 examples how to avoid the "code, code del" antipattern diff -r cb892d835803 -r 2f4491f15fe6 src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Wed Jan 01 01:05:48 2014 +0100 +++ b/src/HOL/Library/Code_Target_Int.thy Wed Jan 01 11:35:21 2014 +0100 @@ -10,8 +10,7 @@ code_datatype int_of_integer -lemma [code, code del]: - "integer_of_int = integer_of_int" .. +declare [[code drop: integer_of_int]] lemma [code]: "integer_of_int (int_of_integer k) = k" @@ -57,8 +56,7 @@ "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))" by transfer simp -lemma [code, code del]: - "Int.sub = Int.sub" .. +declare [[code drop: Int.sub]] lemma [code]: "k * l = int_of_integer (of_int k * of_int l)"