# HG changeset patch # User haftmann # Date 1280311949 -7200 # Node ID 9102e859dc0b7382ae32deaa6cedd666be226fc4 # Parent dc56a9a8e19d4329a3d3cbd12a0f6ea85525f5ab may use `int` in Isabelle runtime environment diff -r dc56a9a8e19d -r 9102e859dc0b src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Tue Jul 27 20:16:14 2010 +0200 +++ b/src/HOL/Library/Code_Integer.thy Wed Jul 28 12:12:29 2010 +0200 @@ -19,6 +19,7 @@ (OCaml "Big'_int.big'_int") (Haskell "Integer") (Scala "BigInt") + (Eval "int") code_instance int :: eq (Haskell -)