src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 59720 f893472fff31
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
wenzelm@59720
     1
(*  Title:      HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
Andreas@58039
     2
    Author:     Andreas Lochbihler, ETH Zurich
Andreas@58039
     3
Andreas@58039
     4
Test case for test_code on SMLNJ
Andreas@58039
     5
*)
Andreas@58039
     6
Andreas@58626
     7
theory Code_Test_SMLNJ imports  "../Library/Code_Test" begin
Andreas@58039
     8
Andreas@58039
     9
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
Andreas@58039
    10
Andreas@58348
    11
value [SMLNJ] "14 + 7 * -12 :: integer"
Andreas@58039
    12
Andreas@58039
    13
end