src/HOL/ex/Codegenerator.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28686 5d63184c10c7
permissions -rw-r--r--
added lemmas
     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