1 (* Title: Pure/Isar/ROOT.ML |
|
2 Author: Markus Wenzel, TU Muenchen |
|
3 |
|
4 Isar -- Intelligible Semi-Automated Reasoning for Isabelle. |
|
5 *) |
|
6 |
|
7 (*proof context*) |
|
8 use "object_logic.ML"; |
|
9 use "rule_cases.ML"; |
|
10 use "auto_bind.ML"; |
|
11 use "local_syntax.ML"; |
|
12 use "proof_context.ML"; |
|
13 use "local_defs.ML"; |
|
14 |
|
15 (*proof term operations*) |
|
16 use "../Proof/reconstruct.ML"; |
|
17 use "../Proof/proof_syntax.ML"; |
|
18 use "../Proof/proof_rewrite_rules.ML"; |
|
19 use "../Proof/proofchecker.ML"; |
|
20 |
|
21 (*outer syntax*) |
|
22 use "outer_lex.ML"; |
|
23 use "outer_keyword.ML"; |
|
24 use "outer_parse.ML"; |
|
25 use "value_parse.ML"; |
|
26 use "args.ML"; |
|
27 |
|
28 (*ML support*) |
|
29 use "../ML/ml_syntax.ML"; |
|
30 use "../ML/ml_env.ML"; |
|
31 if ml_system = "polyml-experimental" |
|
32 then use "../ML/ml_compiler_polyml-5.3.ML" |
|
33 else use "../ML/ml_compiler.ML"; |
|
34 use "../ML/ml_context.ML"; |
|
35 |
|
36 (*theory sources*) |
|
37 use "../Thy/thy_header.ML"; |
|
38 use "../Thy/thy_load.ML"; |
|
39 use "../Thy/html.ML"; |
|
40 use "../Thy/latex.ML"; |
|
41 use "../Thy/present.ML"; |
|
42 |
|
43 (*basic proof engine*) |
|
44 use "proof_display.ML"; |
|
45 use "attrib.ML"; |
|
46 use "../ML/ml_antiquote.ML"; |
|
47 use "context_rules.ML"; |
|
48 use "skip_proof.ML"; |
|
49 use "method.ML"; |
|
50 use "proof.ML"; |
|
51 use "../ML/ml_thms.ML"; |
|
52 use "element.ML"; |
|
53 |
|
54 (*derived theory and proof elements*) |
|
55 use "calculation.ML"; |
|
56 use "obtain.ML"; |
|
57 |
|
58 (*local theories and targets*) |
|
59 use "local_theory.ML"; |
|
60 use "overloading.ML"; |
|
61 use "locale.ML"; |
|
62 use "class_target.ML"; |
|
63 use "theory_target.ML"; |
|
64 use "expression.ML"; |
|
65 use "class.ML"; |
|
66 |
|
67 (*complex proof machineries*) |
|
68 use "../simplifier.ML"; |
|
69 |
|
70 (*executable theory content*) |
|
71 use "code.ML"; |
|
72 |
|
73 (*specifications*) |
|
74 use "spec_parse.ML"; |
|
75 use "specification.ML"; |
|
76 use "constdefs.ML"; |
|
77 |
|
78 (*toplevel transactions*) |
|
79 use "proof_node.ML"; |
|
80 use "toplevel.ML"; |
|
81 |
|
82 (*theory syntax*) |
|
83 use "../Thy/term_style.ML"; |
|
84 use "../Thy/thy_output.ML"; |
|
85 use "../Thy/thy_syntax.ML"; |
|
86 use "../old_goals.ML"; |
|
87 use "outer_syntax.ML"; |
|
88 use "../Thy/thy_info.ML"; |
|
89 use "isar_document.ML"; |
|
90 |
|
91 (*theory and proof operations*) |
|
92 use "rule_insts.ML"; |
|
93 use "../Thy/thm_deps.ML"; |
|
94 use "isar_cmd.ML"; |
|
95 use "isar_syn.ML"; |
|