author | nipkow |
Mon, 27 Feb 2006 14:03:31 +0100 | |
changeset 19147 | 0f584853b6a4 |
parent 19118 | 52f751b50716 |
child 19280 | 5091dc43817b |
permissions | -rw-r--r-- |
16781 | 1 |
(* Title: Pure/Tools/ROOT.ML |
2 |
ID: $Id$ |
|
16842 | 3 |
|
4 |
Miscellaneous tools and packages for Pure Isabelle. |
|
16781 | 5 |
*) |
6 |
||
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
7 |
(*class package*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
8 |
use "class_package.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
9 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
10 |
(*code generator, 1st generation*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
11 |
use "../codegen.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
12 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
13 |
(*code generator, 2nd generation*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
14 |
use "codegen_thingol.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
15 |
use "codegen_serializer.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
16 |
use "codegen_package.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
17 |
|
16842 | 18 |
(*Steven Obua's evaluator*) |
16781 | 19 |
use "am_interpreter.ML"; |
16842 | 20 |
use "am_compiler.ML"; |
16781 | 21 |
use "am_util.ML"; |
22 |
use "compute.ML"; |
|
19118 | 23 |
|
24 |
(* norm-by-eval *) |
|
25 |
use "nbe_eval.ML"; |
|
26 |
use "nbe_codegen.ML"; |
|
19147 | 27 |
use "nbe.ML"; |