src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
changeset 58348 2d47c7d10b62
parent 58039 469a375212c1
child 58626 6c473ed0ac70
equal deleted inserted replaced
58347:272ad6a47d6d 58348:2d47c7d10b62
     6 
     6 
     7 theory Code_Test_SMLNJ imports Code_Test begin
     7 theory Code_Test_SMLNJ imports Code_Test begin
     8 
     8 
     9 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
     9 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
    10 
    10 
    11 eval_term "14 + 7 * -12 :: integer" in SMLNJ
    11 value [SMLNJ] "14 + 7 * -12 :: integer"
    12 
    12 
    13 end
    13 end