author | haftmann |
Mon, 16 Jul 2007 09:29:04 +0200 | |
changeset 23811 | b18557301bf9 |
parent 23266 | 50f0a4f12ed3 |
child 24195 | 7d1a16c77f7c |
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 - |
|
14 |
code_gen in SML to CodegenTest |
|
15 |
in OCaml file - |
|
16 |
in Haskell file - |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
17 |
|
23266 | 18 |
end |