changeset 58660 | 8d4aebb9e327 |
parent 58470 | 890d8286fd4e |
child 58664 | 4e4a4c758f9c |
58659:6c9821c32dd5 | 58660:8d4aebb9e327 |
---|---|
276 use "Isar/expression.ML"; |
276 use "Isar/expression.ML"; |
277 use "Isar/class_declaration.ML"; |
277 use "Isar/class_declaration.ML"; |
278 use "Isar/bundle.ML"; |
278 use "Isar/bundle.ML"; |
279 |
279 |
280 use "simplifier.ML"; |
280 use "simplifier.ML"; |
281 use "Tools/plugin.ML"; |
|
281 |
282 |
282 (*executable theory content*) |
283 (*executable theory content*) |
283 use "Isar/code.ML"; |
284 use "Isar/code.ML"; |
284 |
285 |
285 (*specifications*) |
286 (*specifications*) |