author | haftmann |
Tue, 07 Aug 2007 09:40:34 +0200 | |
changeset 24166 | 7b28dc69bdbb |
parent 24046 | 10f681043e07 |
child 24219 | e558fe311376 |
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*) |
10 |
use "xml.ML"; |
|
22208 | 11 |
use "xml_syntax.ML"; |
20708 | 12 |
|
19812 | 13 |
(*derived theory and proof elements*) |
14 |
use "invoke.ML"; |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
15 |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
16 |
(*code generator, 1st generation*) |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
17 |
use "../codegen.ML"; |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19280
diff
changeset
|
18 |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
19 |
(*code generator, 2nd generation*) |
20353 | 20 |
use "codegen_names.ML"; |
20600 | 21 |
use "codegen_funcgr.ML"; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
22 |
use "codegen_thingol.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
23 |
use "codegen_serializer.ML"; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
16842
diff
changeset
|
24 |
use "codegen_package.ML"; |