src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
author wenzelm
Fri, 18 Aug 2017 20:47:47 +0200
changeset 66453 cc19f7ca2ed6
parent 59720 f893472fff31
child 68155 8b50f29a1992
permissions -rw-r--r--
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

(*  Title:      HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
    Author:     Andreas Lochbihler, ETH Zurich

Test case for test_code on SMLNJ
*)

theory Code_Test_SMLNJ imports  "HOL-Library.Code_Test" begin

test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ

value [SMLNJ] "14 + 7 * -12 :: integer"

end