author | paulson |
Tue, 29 Aug 2017 17:41:27 +0100 | |
changeset 66553 | 6ab32ffb2bdd |
parent 66453 | cc19f7ca2ed6 |
child 68155 | 8b50f29a1992 |
permissions | -rw-r--r-- |
59720 | 1 |
(* Title: HOL/Codegenerator_Test/Code_Test_MLton.thy |
58039 | 2 |
Author: Andreas Lochbihler, ETH Zurich |
3 |
||
4 |
Test case for test_code on MLton |
|
5 |
*) |
|
6 |
||
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
59720
diff
changeset
|
7 |
theory Code_Test_MLton imports "HOL-Library.Code_Test" begin |
58039 | 8 |
|
9 |
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton |
|
10 |
||
58348
2d47c7d10b62
add target language evaluators for the value command;
Andreas Lochbihler
parents:
58039
diff
changeset
|
11 |
value [MLton] "14 + 7 * -12 :: integer" |
58039 | 12 |
|
13 |
end |