| changeset 30142 | 8d6145694bb5 |
| parent 29819 | 29154e67731d |
| child 30174 | eabece26b89b |
| 30141:c59a1258559b | 30142:8d6145694bb5 |
|---|---|
87 use "isar_document.ML"; |
87 use "isar_document.ML"; |
88 |
88 |
89 (*theory and proof operations*) |
89 (*theory and proof operations*) |
90 use "rule_insts.ML"; |
90 use "rule_insts.ML"; |
91 use "../Thy/thm_deps.ML"; |
91 use "../Thy/thm_deps.ML"; |
92 use "find_theorems.ML"; |
|
93 use "find_consts.ML"; |
|
94 use "isar_cmd.ML"; |
92 use "isar_cmd.ML"; |
95 use "isar_syn.ML"; |
93 use "isar_syn.ML"; |