src/HOL/Library/Code_Target_Int.thy
changeset 61275 053ec04ea866
parent 60868 dd18c33c001e
child 61856 4b1b85f38944
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Sun Sep 27 10:11:14 2015 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sun Sep 27 10:11:15 2015 +0200
     1.3 @@ -79,6 +79,11 @@
     1.4    by simp
     1.5  
     1.6  lemma [code]:
     1.7 +  "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
     1.8 +  unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
     1.9 +  by transfer simp
    1.10 +
    1.11 +lemma [code]:
    1.12    "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
    1.13    by transfer (simp add: equal)
    1.14