equal
deleted
inserted
replaced
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Isar -- Intelligible Semi-Automated Reasoning for Isabelle. |
5 Isar -- Intelligible Semi-Automated Reasoning for Isabelle. |
6 *) |
6 *) |
7 |
7 |
8 (*proof engine*) |
8 (*basic proof engine*) |
9 use "auto_bind.ML"; |
9 use "auto_bind.ML"; |
10 use "proof_context.ML"; |
10 use "proof_context.ML"; |
11 use "proof.ML"; |
11 use "proof.ML"; |
12 use "proof_data.ML"; |
12 use "proof_data.ML"; |
13 use "proof_history.ML"; |
13 use "proof_history.ML"; |
14 use "args.ML"; |
14 use "args.ML"; |
15 use "attrib.ML"; |
15 use "attrib.ML"; |
16 use "method.ML"; |
16 use "method.ML"; |
|
17 |
|
18 (*derived proof elements*) |
17 use "calculation.ML"; |
19 use "calculation.ML"; |
|
20 use "skip_proof.ML"; |
18 |
21 |
19 (*outer syntax*) |
22 (*outer syntax*) |
20 use "comment.ML"; |
23 use "comment.ML"; |
21 use "outer_lex.ML"; |
24 use "outer_lex.ML"; |
22 use "outer_parse.ML"; |
25 use "outer_parse.ML"; |