src/HOL/ex/Codegenerator.thy
changeset 28686 5d63184c10c7
parent 28335 25326092cf9a
equal deleted inserted replaced
28685:275122631271 28686:5d63184c10c7
    12 nonfix union;
    12 nonfix union;
    13 nonfix inter;
    13 nonfix inter;
    14 nonfix upto;
    14 nonfix upto;
    15 *}
    15 *}
    16 
    16 
    17 export_code "RType.*" -- "workaround for cache problem"
       
    18 export_code * in SML module_name CodegenTest
    17 export_code * in SML module_name CodegenTest
    19   in OCaml module_name CodegenTest file -
    18   in OCaml module_name CodegenTest file -
    20   in Haskell file -
    19   in Haskell file -
    21 
    20 
    22 ML {*
    21 ML {*