src/HOL/Library/Code_Target_Int.thy

 lemma [code]:
   "k * l = int_of_integer (of_int k * of_int l)"
   by simp
 
 lemma [code]:
-  "Divides.divmod_abs k l = map_prod int_of_integer int_of_integer
-    (Code_Numeral.divmod_abs (of_int k) (of_int l))"
-  by (simp add: prod_eq_iff)
-
-lemma [code]:
   "k div l = int_of_integer (of_int k div of_int l)"
   by simp
 
 lemma [code]:
   "k mod l = int_of_integer (of_int k mod of_int l)"

 
 lemma (in ring_1) of_int_code_if:
   "of_int k = (if k = 0 then 0
      else if k < 0 then - of_int (- k)
      else let
-       (l, j) = divmod_int k 2;
-       l' = 2 * of_int l
-     in if j = 0 then l' else l' + 1)"
+       l = 2 * of_int (k div 2);
+       j = k mod 2
+     in if j = 0 then l else l + 1)"
 proof -
   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   show ?thesis
-    by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric])
-      (simp add: * mult.commute)
+    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
 qed
 
 declare of_int_code_if [code]
 
 lemma [code]:

 code_identifier
   code_module Code_Target_Int \<rightharpoonup>
     (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-