| changeset 29819 | 29154e67731d |
| parent 29576 | 669b560fc2b9 |
| child 30142 | 8d6145694bb5 |
| child 30240 | 5b25fee0362c |
| 29818:58f3c48dbbb7 | 29819:29154e67731d |
|---|---|
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"; |
92 use "find_theorems.ML"; |
93 use "find_consts.ML"; |
|
93 use "isar_cmd.ML"; |
94 use "isar_cmd.ML"; |
94 use "isar_syn.ML"; |
95 use "isar_syn.ML"; |