equal
deleted
inserted
replaced
41 use "proof.ML"; |
41 use "proof.ML"; |
42 use "element.ML"; |
42 use "element.ML"; |
43 use "net_rules.ML"; |
43 use "net_rules.ML"; |
44 use "induct_attrib.ML"; |
44 use "induct_attrib.ML"; |
45 |
45 |
46 (*code generator base*) |
46 (*executable theory content*) |
47 use "../Tools/codegen_consts.ML"; |
47 use "code_unit.ML"; |
48 use "../Tools/codegen_func.ML"; |
48 use "code.ML"; |
49 use "../Tools/codegen_data.ML"; |
|
50 |
49 |
51 (*derived theory and proof elements*) |
50 (*derived theory and proof elements*) |
52 use "local_theory.ML"; |
51 use "local_theory.ML"; |
53 use "calculation.ML"; |
52 use "calculation.ML"; |
54 use "obtain.ML"; |
53 use "obtain.ML"; |
55 use "locale.ML"; |
54 use "locale.ML"; |
56 use "spec_parse.ML"; |
55 use "spec_parse.ML"; |
57 use "../Tools/class_package.ML"; |
56 use "class.ML"; |
58 use "theory_target.ML"; |
57 use "theory_target.ML"; |
59 use "specification.ML"; |
58 use "specification.ML"; |
60 use "constdefs.ML"; |
59 use "constdefs.ML"; |
61 |
60 |
62 (*toplevel environment*) |
61 (*toplevel environment*) |