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