src/HOL/ex/Codegenerator.thy
changeset 24432 d555d941f983
parent 24430 df56b9779a3d
child 24718 16b11ba36350
equal deleted inserted replaced
24431:02d29baa42ff 24432:d555d941f983
     6 
     6 
     7 theory Codegenerator
     7 theory Codegenerator
     8 imports ExecutableContent
     8 imports ExecutableContent
     9 begin
     9 begin
    10 
    10 
    11 ML {*
    11 ML {* (*FIXME get rid of this*)
    12 nonfix union;
    12 nonfix union;
    13 nonfix inter;
    13 nonfix inter;
    14 *}
    14 *}
    15 
    15 
    16 export_code * in SML module_name CodegenTest
    16 export_code * in SML module_name CodegenTest
    17   in OCaml file -
    17   in OCaml file -
    18   in Haskell file -
    18   in Haskell file -
    19 
    19 
       
    20 ML {*
       
    21 infix union;
       
    22 infix inter;
       
    23 *}
       
    24 
    20 end
    25 end