src/HOL/ex/Codegenerator.thy
author wenzelm
Fri, 15 Aug 2008 15:50:52 +0200
changeset 27885 76b51cd0a37c
parent 24810 862b71696efe
child 28335 25326092cf9a
permissions -rw-r--r--
renamed T.source_of' to T.source_position_of;

(*  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;
nonfix upto;
*}

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

ML {*
infix union;
infix inter;
infix 4 upto;
*}

end