| changeset 31156 | 90fed3d4430f |
| parent 30590 | ad19c99529eb |
| child 31369 | ba5b7749fa61 |
| 31155:92d8ff6af82c | 31156:90fed3d4430f |
|---|---|
59 |
59 |
60 (*complex proof machineries*) |
60 (*complex proof machineries*) |
61 use "../simplifier.ML"; |
61 use "../simplifier.ML"; |
62 |
62 |
63 (*executable theory content*) |
63 (*executable theory content*) |
64 use "code_unit.ML"; |
|
65 use "code.ML"; |
64 use "code.ML"; |
66 |
65 |
67 (*specifications*) |
66 (*specifications*) |
68 use "spec_parse.ML"; |
67 use "spec_parse.ML"; |
69 use "specification.ML"; |
68 use "specification.ML"; |