1.1 --- a/src/HOL/Library/Code_Integer.thy	Mon Feb 16 13:38:17 2009 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Feb 16 19:11:15 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Library/Code_Integer.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Florian Haftmann, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -72,6 +71,11 @@
    1.10    (OCaml "Big'_int.mult'_big'_int")
    1.11    (Haskell infixl 7 "*")
    1.12  
    1.13 +code_const pdivmod
    1.14 +  (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
    1.15 +  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
    1.16 +  (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
    1.17 +
    1.18  code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.19    (SML "!((_ : IntInf.int) = _)")
    1.20    (OCaml "Big'_int.eq'_big'_int")