equal
deleted
inserted
replaced
79 use "../Thy/term_style.ML"; |
79 use "../Thy/term_style.ML"; |
80 use "../Thy/thy_output.ML"; |
80 use "../Thy/thy_output.ML"; |
81 use "../old_goals.ML"; |
81 use "../old_goals.ML"; |
82 use "outer_syntax.ML"; |
82 use "outer_syntax.ML"; |
83 use "../Thy/thy_info.ML"; |
83 use "../Thy/thy_info.ML"; |
|
84 use "../Thy/thy_edit.ML"; |
84 use "session.ML"; |
85 use "session.ML"; |
85 use "isar.ML"; |
86 use "isar.ML"; |
86 use "../Thy/thy_edit.ML"; |
|
87 |
87 |
88 (*theory and proof operations*) |
88 (*theory and proof operations*) |
89 use "rule_insts.ML"; |
89 use "rule_insts.ML"; |
90 use "../Thy/thm_deps.ML"; |
90 use "../Thy/thm_deps.ML"; |
91 use "find_theorems.ML"; |
91 use "find_theorems.ML"; |