equal
deleted
inserted
replaced
9 (*basic XML support*) |
9 (*basic XML support*) |
10 use "xml_syntax.ML"; |
10 use "xml_syntax.ML"; |
11 |
11 |
12 (*derived theory and proof elements*) |
12 (*derived theory and proof elements*) |
13 use "invoke.ML"; |
13 use "invoke.ML"; |
14 |
|
15 (*code generator*) |
|
16 use "../codegen.ML"; |
|
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"; |
|