equal
deleted
inserted
replaced
48 |
48 |
49 (*derived theory and proof elements*) |
49 (*derived theory and proof elements*) |
50 use "calculation.ML"; |
50 use "calculation.ML"; |
51 use "obtain.ML"; |
51 use "obtain.ML"; |
52 |
52 |
53 (*local theories and target primitives*) |
53 (*local theories and targets*) |
54 use "local_theory.ML"; |
54 use "local_theory.ML"; |
55 use "overloading.ML"; |
55 use "overloading.ML"; |
56 use "locale.ML"; |
56 use "locale.ML"; |
57 use "class.ML"; |
57 use "class.ML"; |
|
58 use "theory_target.ML"; |
|
59 use "instance.ML"; |
|
60 use "subclass.ML"; |
58 |
61 |
59 (*complex proof machineries*) |
62 (*complex proof machineries*) |
60 use "../simplifier.ML"; |
63 use "../simplifier.ML"; |
61 |
64 |
62 (*executable theory content*) |
65 (*executable theory content*) |
63 use "code_unit.ML"; |
66 use "code_unit.ML"; |
64 use "code.ML"; |
67 use "code.ML"; |
65 |
68 |
66 (*local theories and specifications*) |
69 (*specifications*) |
67 use "theory_target.ML"; |
|
68 use "subclass.ML"; |
|
69 use "spec_parse.ML"; |
70 use "spec_parse.ML"; |
70 use "specification.ML"; |
71 use "specification.ML"; |
71 use "instance.ML"; |
|
72 use "constdefs.ML"; |
72 use "constdefs.ML"; |
73 |
73 |
74 (*toplevel transactions*) |
74 (*toplevel transactions*) |
75 use "proof_node.ML"; |
75 use "proof_node.ML"; |
76 use "toplevel.ML"; |
76 use "toplevel.ML"; |