changeset 58039 | 469a375212c1 |
child 58348 | 2d47c7d10b62 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,13 @@ +(* Title: Code_Test_PolyML.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on PolyML +*) + +theory Code_Test_PolyML imports Code_Test begin + +test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML + +eval_term "14 + 7 * -12 :: integer" in PolyML + +end