author | blanchet |
Wed, 03 Sep 2014 00:06:24 +0200 | |
changeset 58152 | 6fe60a9a5bad |
parent 58039 | 469a375212c1 |
child 58348 | 2d47c7d10b62 |
permissions | -rw-r--r-- |
(* Title: Code_Test_GHC.thy Author: Andreas Lochbihler, ETH Zurich Test case for test_code on GHC *) theory Code_Test_GHC imports Code_Test begin definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id" test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC eval_term "14 + 7 * -12 :: integer" in GHC end