src/HOL/Library/Code_Integer.thy

--- a/src/HOL/Library/Code_Integer.thy	Mon Feb 16 13:38:17 2009 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Mon Feb 16 19:11:15 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Code_Integer.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
@@ -72,6 +71,11 @@
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
+code_const pdivmod
+  (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
+  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
+  (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
+
 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")