src/HOL/ex/Codegenerator.thy
changeset 31378 d1cbf6393964
parent 31377 a48f9ef9de15
child 31379 213299656575
equal deleted inserted replaced
31377:a48f9ef9de15 31378:d1cbf6393964
     1 (*  ID:         $Id$
       
     2     Author:     Florian Haftmann, TU Muenchen
       
     3 *)
       
     4 
       
     5 header {* Tests and examples for code generator *}
       
     6 
       
     7 theory Codegenerator
       
     8 imports ExecutableContent
       
     9 begin
       
    10 
       
    11 ML {* (*FIXME get rid of this*)
       
    12 nonfix union;
       
    13 nonfix inter;
       
    14 nonfix upto;
       
    15 *}
       
    16 
       
    17 export_code * in SML module_name CodegenTest
       
    18   in OCaml module_name CodegenTest file -
       
    19   in Haskell file -
       
    20 
       
    21 ML {*
       
    22 infix union;
       
    23 infix inter;
       
    24 infix 4 upto;
       
    25 *}
       
    26 
       
    27 end