| author | haftmann |
| Fri, 02 Jul 2010 14:23:18 +0200 | |
| changeset 37686 | 71e84a203c19 |
| parent 34302 | src/HOL/ex/Codegenerator_Test.thy@e8b8ee60c1e2 |
| child 37744 | 6315b6426200 |
| permissions | -rw-r--r-- |
| haftmann@19281 | 1 |
|
| haftmann@31378 | 2 |
(* Author: Florian Haftmann, TU Muenchen *) |
| haftmann@19281 | 3 |
|
| haftmann@31378 | 4 |
header {* Pervasive test of code generator *}
|
| haftmann@31378 | 5 |
|
| haftmann@37686 | 6 |
theory Generate |
| haftmann@37686 | 7 |
imports Candidates |
| haftmann@19281 | 8 |
begin |
| haftmann@19281 | 9 |
|
| haftmann@37686 | 10 |
export_code * in SML module_name Code_Test |
| haftmann@37686 | 11 |
in OCaml module_name Code_Test file - |
| haftmann@23811 | 12 |
in Haskell file - |
| haftmann@34302 | 13 |
in Scala file - |
| haftmann@19281 | 14 |
|
| wenzelm@23266 | 15 |
end |