equal
deleted
inserted
replaced
|
1 (* Title: Pure/Isar/ROOT.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Isar -- Intelligible Semi-Automated Reasoning for Isabelle. |
|
6 *) |
|
7 |
|
8 (*proof engine*) |
|
9 use "proof_context.ML"; |
|
10 use "proof.ML"; |
|
11 use "proof_data.ML"; |
|
12 use "args.ML"; |
|
13 use "attrib.ML"; |
|
14 use "method.ML"; |
|
15 |
|
16 (*outer syntax*) |
|
17 use "outer_lex.ML"; |
|
18 use "outer_parse.ML"; |
|
19 |
|
20 (*interactive subsystem*) |
|
21 use "proof_history.ML"; |
|
22 use "toplevel.ML"; |
|
23 use "outer_syntax.ML"; |
|
24 |
|
25 (*theory operations and syntax*) |
|
26 use "isar_thy.ML"; |
|
27 use "isar_cmd.ML"; |
|
28 use "isar_syn.ML"; |