1.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 10:25:00 2010 +0200
1.2 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 10:58:13 2010 +0200
1.3 @@ -412,13 +412,13 @@
1.4 code_const Code_Numeral.of_nat
1.5 (SML "IntInf.toInt")
1.6 (OCaml "_")
1.7 - (Haskell "fromEnum")
1.8 + (Haskell "toInteger")
1.9 (Scala "!_.as'_Int")
1.10
1.11 code_const Code_Numeral.nat_of
1.12 (SML "IntInf.fromInt")
1.13 (OCaml "_")
1.14 - (Haskell "toEnum")
1.15 + (Haskell "fromInteger")
1.16 (Scala "Nat")
1.17
1.18 text {* Using target language arithmetic operations whenever appropriate *}