changeset 31377 | a48f9ef9de15 |
parent 31295 | 956592c2c701 |
child 31954 | 8db19c99b00a |
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 02 15:53:04 2009 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 02 15:53:05 2009 +0200 @@ -371,12 +371,12 @@ code_const Code_Numeral.of_nat (SML "IntInf.toInt") - (OCaml "Big'_int.int'_of'_big'_int") + (OCaml "_") (Haskell "fromEnum") code_const Code_Numeral.nat_of (SML "IntInf.fromInt") - (OCaml "Big'_int.big'_int'_of'_int") + (OCaml "_") (Haskell "toEnum") text {* Using target language arithmetic operations whenever appropriate *}