| author | wenzelm |
| Tue, 04 Jul 2006 19:49:47 +0200 | |
| changeset 19997 | fe69952f09f6 |
| parent 19884 | a7be206d8655 |
| child 20105 | 454f4be984b7 |
| 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 |
||
| 19812 | 7 |
(*derived theory and proof elements*) |
8 |
use "invoke.ML"; |
|
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
9 |
use "class_package.ML"; |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
10 |
|
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
11 |
(*code generator, 1st generation*) |
|
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
12 |
use "../codegen.ML"; |
|
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
13 |
|
|
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19147
diff
changeset
|
14 |
(*code generator theorems*) |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19147
diff
changeset
|
15 |
use "codegen_theorems.ML"; |
| 19884 | 16 |
use "codegen_simtype.ML"; |
|
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19147
diff
changeset
|
17 |
|
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
18 |
(*code generator, 2nd generation*) |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
19 |
use "codegen_thingol.ML"; |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
20 |
use "codegen_serializer.ML"; |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
21 |
use "codegen_package.ML"; |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
22 |
|
| 16842 | 23 |
(*Steven Obua's evaluator*) |
| 16781 | 24 |
use "am_interpreter.ML"; |
| 16842 | 25 |
use "am_compiler.ML"; |
| 16781 | 26 |
use "am_util.ML"; |
27 |
use "compute.ML"; |
|
| 19118 | 28 |
|
| 19812 | 29 |
(*norm-by-eval*) |
| 19118 | 30 |
use "nbe_eval.ML"; |
31 |
use "nbe_codegen.ML"; |
|
| 19147 | 32 |
use "nbe.ML"; |