use module integer for Eval
authorhaftmann
Fri Oct 01 14:15:49 2010 +0200 (2010-10-01)
changeset 39818ff9e9d5ac171
parent 39817 5228c6b20273
child 39819 6ddbd932fc00
child 39903 06fde6521972
child 39910 10097e0a9dbd
use module integer for Eval
src/HOL/Code_Numeral.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Oct 01 11:46:09 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Oct 01 14:15:49 2010 +0200
     1.3 @@ -340,7 +340,7 @@
     1.4    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
     1.5    (Haskell "divMod")
     1.6    (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
     1.7 -  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
     1.8 +  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))")
     1.9  
    1.10  code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.11    (SML "!((_ : Int.int) = _)")