equal
deleted
inserted
replaced
25 use "../Thy/thy_header.ML"; |
25 use "../Thy/thy_header.ML"; |
26 use "../Thy/thy_load.ML"; |
26 use "../Thy/thy_load.ML"; |
27 use "../Thy/html.ML"; |
27 use "../Thy/html.ML"; |
28 use "../Thy/latex.ML"; |
28 use "../Thy/latex.ML"; |
29 use "../Thy/present.ML"; |
29 use "../Thy/present.ML"; |
30 use "../Thy/thy_info.ML"; |
|
31 use "../Thy/thm_deps.ML"; |
|
32 |
30 |
33 (*basic proof engine*) |
31 (*basic proof engine*) |
34 use "proof_display.ML"; |
32 use "proof_display.ML"; |
35 use "attrib.ML"; |
33 use "attrib.ML"; |
36 use "context_rules.ML"; |
34 use "context_rules.ML"; |
60 use "spec_parse.ML"; |
58 use "spec_parse.ML"; |
61 use "specification.ML"; |
59 use "specification.ML"; |
62 use "instance.ML"; |
60 use "instance.ML"; |
63 use "constdefs.ML"; |
61 use "constdefs.ML"; |
64 |
62 |
65 (*toplevel environment*) |
63 (*toplevel transactions*) |
66 use "proof_history.ML"; |
64 use "proof_history.ML"; |
67 use "toplevel.ML"; |
65 use "toplevel.ML"; |
68 |
66 |
69 (*theory presentation*) |
67 (*theory syntax*) |
70 use "../Thy/term_style.ML"; |
68 use "../Thy/term_style.ML"; |
71 use "../Thy/thy_output.ML"; |
69 use "../Thy/thy_output.ML"; |
72 |
|
73 (*theory syntax*) |
|
74 use "session.ML"; |
|
75 use "../old_goals.ML"; |
70 use "../old_goals.ML"; |
76 use "outer_syntax.ML"; |
71 use "outer_syntax.ML"; |
|
72 use "../Thy/thy_info.ML"; |
|
73 use "session.ML"; |
77 use "isar.ML"; |
74 use "isar.ML"; |
78 use "../Thy/thy_edit.ML"; |
75 use "../Thy/thy_edit.ML"; |
79 |
76 |
80 (*theory and proof operations*) |
77 (*theory and proof operations*) |
81 use "rule_insts.ML"; |
78 use "rule_insts.ML"; |
82 use "../simplifier.ML"; |
79 use "../simplifier.ML"; |
|
80 use "../Thy/thm_deps.ML"; |
83 use "find_theorems.ML"; |
81 use "find_theorems.ML"; |
84 use "isar_cmd.ML"; |
82 use "isar_cmd.ML"; |
85 use "isar_syn.ML"; |
83 use "isar_syn.ML"; |