equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 Miscellaneous tools and packages for Pure Isabelle. |
4 Miscellaneous tools and packages for Pure Isabelle. |
5 *) |
5 *) |
6 |
6 |
7 (*class package*) |
7 (*derived theory and proof elements*) |
|
8 use "invoke.ML"; |
8 use "class_package.ML"; |
9 use "class_package.ML"; |
9 |
10 |
10 (*code generator, 1st generation*) |
11 (*code generator, 1st generation*) |
11 use "../codegen.ML"; |
12 use "../codegen.ML"; |
12 |
13 |
22 use "am_interpreter.ML"; |
23 use "am_interpreter.ML"; |
23 use "am_compiler.ML"; |
24 use "am_compiler.ML"; |
24 use "am_util.ML"; |
25 use "am_util.ML"; |
25 use "compute.ML"; |
26 use "compute.ML"; |
26 |
27 |
27 (* norm-by-eval *) |
28 (*norm-by-eval*) |
28 use "nbe_eval.ML"; |
29 use "nbe_eval.ML"; |
29 use "nbe_codegen.ML"; |
30 use "nbe_codegen.ML"; |
30 use "nbe.ML"; |
31 use "nbe.ML"; |