src/HOL/ex/Codegenerator.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 24810 862b71696efe
child 28335 25326092cf9a
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
haftmann@19281
     1
(*  ID:         $Id$
haftmann@19281
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@19281
     3
*)
haftmann@19281
     4
haftmann@21877
     5
header {* Tests and examples for code generator *}
haftmann@19281
     6
haftmann@19281
     7
theory Codegenerator
haftmann@21911
     8
imports ExecutableContent
haftmann@19281
     9
begin
haftmann@19281
    10
haftmann@24432
    11
ML {* (*FIXME get rid of this*)
haftmann@24430
    12
nonfix union;
haftmann@24430
    13
nonfix inter;
haftmann@24718
    14
nonfix upto;
haftmann@24430
    15
*}
haftmann@24430
    16
haftmann@24423
    17
export_code * in SML module_name CodegenTest
haftmann@24810
    18
  in OCaml module_name CodegenTest file -
haftmann@23811
    19
  in Haskell file -
haftmann@19281
    20
haftmann@24432
    21
ML {*
haftmann@24432
    22
infix union;
haftmann@24432
    23
infix inter;
haftmann@24718
    24
infix 4 upto;
haftmann@24432
    25
*}
haftmann@24432
    26
wenzelm@23266
    27
end