| author | wenzelm |
| Tue, 14 Aug 2007 13:20:47 +0200 | |
| changeset 24264 | d6935e7dac8b |
| parent 24219 | e558fe311376 |
| child 24280 | c9867bdf2424 |
| 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 |
||
| 24046 | 7 |
use "named_thms.ML"; |
8 |
||
| 23614 | 9 |
(*basic XML support*) |
| 22208 | 10 |
use "xml_syntax.ML"; |
| 20708 | 11 |
|
| 19812 | 12 |
(*derived theory and proof elements*) |
13 |
use "invoke.ML"; |
|
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
14 |
|
| 24219 | 15 |
(*code generator*) |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
16 |
use "../codegen.ML"; |
| 24219 | 17 |
use "../../Tools/code/code_name.ML"; |
18 |
use "../../Tools/code/code_funcgr.ML"; |
|
19 |
use "../../Tools/code/code_thingol.ML"; |
|
20 |
use "../../Tools/code/code_target.ML"; |
|
21 |
use "../../Tools/code/code_package.ML"; |