| changeset 58348 | 2d47c7d10b62 |
| parent 58039 | 469a375212c1 |
| child 58414 | f945e7af0d27 |
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Mon Sep 15 18:12:09 2014 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Tue Sep 16 16:04:08 2014 +0200 @@ -10,6 +10,6 @@ test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC -eval_term "14 + 7 * -12 :: integer" in GHC +value [GHC] "14 + 7 * -12 :: integer" end