src/HOL/ex/Codegenerator.thy
author berghofe
Tue, 28 Aug 2007 18:23:59 +0200
changeset 24461 bbff04c027ec
parent 24432 d555d941f983
child 24718 16b11ba36350
permissions -rw-r--r--
Changed "code" attribute of concat_map_singleton to "code unfold".

(*  ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen
*)

header {* Tests and examples for code generator *}

theory Codegenerator
imports ExecutableContent
begin

ML {* (*FIXME get rid of this*)
nonfix union;
nonfix inter;
*}

export_code * in SML module_name CodegenTest
  in OCaml file -
  in Haskell file -

ML {*
infix union;
infix inter;
*}

end