changeset 55932 | 68c5104d2204 |
parent 55736 | f1ed1e9cd080 |
child 57512 | cc97b347b301 |
--- a/src/HOL/Library/Code_Target_Int.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Library/Code_Target_Int.thy Thu Mar 06 13:36:48 2014 +0100 @@ -67,7 +67,7 @@ by simp lemma [code]: - "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer + "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)