author | haftmann |
Thu, 09 Aug 2007 15:52:45 +0200 | |
changeset 24195 | 7d1a16c77f7c |
parent 23811 | b18557301bf9 |
child 24249 | 1f60b45c5f97 |
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 |
|
23811 | 11 |
code_gen "*" in SML to CodegenTest |
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 |