src/HOL/ex/Codegenerator.thy
author haftmann
Fri Oct 24 17:48:39 2008 +0200 (2008-10-24)
changeset 28686 5d63184c10c7
parent 28335 25326092cf9a
permissions -rw-r--r--
tuned
     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