author | haftmann |
Fri, 24 Aug 2007 14:14:20 +0200 | |
changeset 24423 | ae9cd0e92423 |
parent 24348 | c708ea5b109a |
child 24430 | df56b9779a3d |
permissions | -rw-r--r-- |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
3 |
*) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
4 |
|
21877
e871f57b1adb
now testing executable content of nearly all HOL
haftmann
parents:
21545
diff
changeset
|
5 |
header {* Tests and examples for code generator *} |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
6 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
7 |
theory Codegenerator |
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21898
diff
changeset
|
8 |
imports ExecutableContent |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
9 |
begin |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
10 |
|
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24348
diff
changeset
|
11 |
export_code * in SML module_name CodegenTest |
23811 | 12 |
in OCaml file - |
13 |
in Haskell file - |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
14 |
|
23266 | 15 |
end |