author | haftmann |
Mon, 13 Aug 2007 21:22:37 +0200 | |
changeset 24249 | 1f60b45c5f97 |
parent 24195 | 7d1a16c77f7c |
child 24348 | c708ea5b109a |
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 |
|
24249 | 11 |
code_gen "*" 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 |