src/HOL/Codegenerator_Test/Code_Test_MLton.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
     1 (*  Title:      HOL/Codegenerator_Test/Code_Test_MLton.thy
     2     Author:     Andreas Lochbihler, ETH Zurich
     3 
     4 Test case for test_code on MLton
     5 *)
     6 
     7 theory Code_Test_MLton imports  "../Library/Code_Test" begin
     8 
     9 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton
    10 
    11 value [MLton] "14 + 7 * -12 :: integer"
    12 
    13 end