author | aspinall |
Tue, 19 Dec 2006 17:35:33 +0100 | |
changeset 21886 | f1790ca921e1 |
parent 20939 | a81ce849e9f4 |
child 22023 | 487b79b95a20 |
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 |
||
20708 | 7 |
|
19812 | 8 |
(*derived theory and proof elements*) |
9 |
use "invoke.ML"; |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
10 |
use "class_package.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
11 |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
12 |
(*code generator, 1st generation*) |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
13 |
use "../codegen.ML"; |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
14 |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
15 |
(*code generator, 2nd generation*) |
20384 | 16 |
use "codegen_consts.ML"; |
20708 | 17 |
use "codegen_data.ML"; |
20353 | 18 |
use "codegen_names.ML"; |
20600 | 19 |
use "codegen_funcgr.ML"; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
20 |
use "codegen_thingol.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
21 |
use "codegen_serializer.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
22 |
use "codegen_package.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
23 |
|
16842 | 24 |
(*Steven Obua's evaluator*) |
16781 | 25 |
use "am_interpreter.ML"; |
16842 | 26 |
use "am_compiler.ML"; |
16781 | 27 |
use "am_util.ML"; |
28 |
use "compute.ML"; |
|
19118 | 29 |
|
19812 | 30 |
(*norm-by-eval*) |
19118 | 31 |
use "nbe_eval.ML"; |
32 |
use "nbe_codegen.ML"; |
|
19147 | 33 |
use "nbe.ML"; |
20657 | 34 |
|
35 |
(*XML syntax for terms and types*) |
|
36 |
use "xml_syntax.ML"; |