changeset 37947 | 844977c7abeb |
parent 37892 | 3d8857f42a64 |
child 37958 | 9728342bcd56 |
--- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 10:25:00 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 10:58:13 2010 +0200 @@ -412,13 +412,13 @@ code_const Code_Numeral.of_nat (SML "IntInf.toInt") (OCaml "_") - (Haskell "fromEnum") + (Haskell "toInteger") (Scala "!_.as'_Int") code_const Code_Numeral.nat_of (SML "IntInf.fromInt") (OCaml "_") - (Haskell "toEnum") + (Haskell "fromInteger") (Scala "Nat") text {* Using target language arithmetic operations whenever appropriate *}