changeset 28288 | 09c812966e7f |
parent 28200 | 5ef2c4bde4e5 |
child 28318 | 6b8d001ce1de |
28287:c86fa4e0aedb | 28288:09c812966e7f |
---|---|
59 use "pattern.ML"; |
59 use "pattern.ML"; |
60 use "unify.ML"; |
60 use "unify.ML"; |
61 use "theory.ML"; |
61 use "theory.ML"; |
62 use "interpretation.ML"; |
62 use "interpretation.ML"; |
63 use "proofterm.ML"; |
63 use "proofterm.ML"; |
64 use "deriv.ML"; |
|
64 use "thm.ML"; |
65 use "thm.ML"; |
65 use "more_thm.ML"; |
66 use "more_thm.ML"; |
66 use "facts.ML"; |
67 use "facts.ML"; |
67 use "pure_thy.ML"; |
68 use "pure_thy.ML"; |
68 use "display.ML"; |
69 use "display.ML"; |