changeset 29815 | 9e94b7078fa5 |
parent 29793 | 86cac1fab613 |
child 29932 | a2594b5c945a |
--- a/src/HOL/Library/Efficient_Nat.thy Fri Feb 06 09:05:19 2009 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Feb 06 09:05:19 2009 +0100 @@ -376,12 +376,12 @@ text {* Conversion from and to indices. *} -code_const index_of_nat +code_const Code_Index.of_nat (SML "IntInf.toInt") (OCaml "Big'_int.int'_of'_big'_int") (Haskell "fromEnum") -code_const nat_of_index +code_const Code_Index.nat_of (SML "IntInf.fromInt") (OCaml "Big'_int.big'_int'_of'_int") (Haskell "toEnum")