--- a/src/HOL/Library/Code_Target_Int.thy Tue Feb 25 17:06:17 2014 +0000
+++ b/src/HOL/Library/Code_Target_Int.thy Tue Feb 25 19:07:14 2014 +0100
@@ -12,6 +12,10 @@
declare [[code drop: integer_of_int]]
+context
+includes integer.lifting
+begin
+
lemma [code]:
"integer_of_int (int_of_integer k) = k"
by transfer rule
@@ -86,6 +90,7 @@
lemma [code]:
"k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
by transfer rule
+end
lemma (in ring_1) of_int_code_if:
"of_int k = (if k = 0 then 0
@@ -105,7 +110,7 @@
lemma [code]:
"nat = nat_of_integer \<circ> of_int"
- by transfer (simp add: fun_eq_iff)
+ including integer.lifting by transfer (simp add: fun_eq_iff)
code_identifier
code_module Code_Target_Int \<rightharpoonup>