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