author  ballarin 
Wed, 19 Nov 2008 16:58:33 +0100  
changeset 28849  9458d7a6388a 
parent 28795  6891e273c33b 
child 29249  4dc278c8dc59 
permissions  rwrr 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Isar/ROOT.ML 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

4 

962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

5 
Isar  Intelligible SemiAutomated Reasoning for Isabelle. 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

6 
*) 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

7 

19382  8 
(*proof context*) 
11889  9 
use "object_logic.ML"; 
17348  10 
use "rule_cases.ML"; 
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
6771
diff
changeset

11 
use "auto_bind.ML"; 
18990  12 
use "local_syntax.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

13 
use "proof_context.ML"; 
18819  14 
use "local_defs.ML"; 
19382  15 

27254  16 
(*proof term operations*) 
17 
use "../Proof/reconstruct.ML"; 

18 
use "../Proof/proof_syntax.ML"; 

19 
use "../Proof/proof_rewrite_rules.ML"; 

20 
use "../Proof/proofchecker.ML"; 

21 

22113
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

22 
(*outer syntax*) 
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

23 
use "outer_lex.ML"; 
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

24 
use "outer_parse.ML"; 
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

25 
use "outer_keyword.ML"; 
27810  26 
use "args.ML"; 
22113
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

27 
use "antiquote.ML"; 
24574  28 
use "../ML/ml_context.ML"; 
22113
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

29 

4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

30 
(*theory sources*) 
23864  31 
use "../Thy/thy_header.ML"; 
22113
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

32 
use "../Thy/thy_load.ML"; 
19382  33 
use "../Thy/html.ML"; 
34 
use "../Thy/latex.ML"; 

35 
use "../Thy/present.ML"; 

36 

37 
(*basic proof engine*) 

17348  38 
use "proof_display.ML"; 
15703  39 
use "attrib.ML"; 
27339  40 
use "../ML/ml_antiquote.ML"; 
18634  41 
use "context_rules.ML"; 
17348  42 
use "skip_proof.ML"; 
17103  43 
use "method.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

44 
use "proof.ML"; 
27394  45 
use "../ML/ml_thms.ML"; 
18128  46 
use "element.ML"; 
8298  47 
use "net_rules.ML"; 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6783
diff
changeset

48 

17348  49 
(*derived theory and proof elements*) 
18741  50 
use "calculation.ML"; 
51 
use "obtain.ML"; 

25462  52 

27685  53 
(*local theories and targets*) 
28849  54 
val new_locales = ref false; 
25462  55 
use "local_theory.ML"; 
25519  56 
use "overloading.ML"; 
18741  57 
use "locale.ML"; 
28795  58 
use "new_locale.ML"; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
27837
diff
changeset

59 
use "expression.ML"; 
24306  60 
use "class.ML"; 
27685  61 
use "theory_target.ML"; 
62 
use "instance.ML"; 

63 
use "subclass.ML"; 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24306
diff
changeset

64 

27581  65 
(*complex proof machineries*) 
66 
use "../simplifier.ML"; 

67 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24306
diff
changeset

68 
(*executable theory content*) 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24306
diff
changeset

69 
use "code_unit.ML"; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24306
diff
changeset

70 
use "code.ML"; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24306
diff
changeset

71 

27685  72 
(*specifications*) 
22113
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

73 
use "spec_parse.ML"; 
18613  74 
use "specification.ML"; 
17348  75 
use "constdefs.ML"; 
18741  76 

26609
53754d9ee31f
load thy_info.ML after outer_syntax.ML  avoids backpatching of load_thy;
wenzelm
parents:
26598
diff
changeset

77 
(*toplevel transactions*) 
27559  78 
use "proof_node.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

79 
use "toplevel.ML"; 
17058  80 

26609
53754d9ee31f
load thy_info.ML after outer_syntax.ML  avoids backpatching of load_thy;
wenzelm
parents:
26598
diff
changeset

81 
(*theory syntax*) 
22113
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

82 
use "../Thy/term_style.ML"; 
4a65d2f4d0b5
renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
21739
diff
changeset

83 
use "../Thy/thy_output.ML"; 
27837  84 
use "../Thy/thy_edit.ML"; 
18116  85 
use "../old_goals.ML"; 
12936  86 
use "outer_syntax.ML"; 
26609
53754d9ee31f
load thy_info.ML after outer_syntax.ML  avoids backpatching of load_thy;
wenzelm
parents:
26598
diff
changeset

87 
use "../Thy/thy_info.ML"; 
53754d9ee31f
load thy_info.ML after outer_syntax.ML  avoids backpatching of load_thy;
wenzelm
parents:
26598
diff
changeset

88 
use "session.ML"; 
26598  89 
use "isar.ML"; 
12936  90 

8091  91 
(*theory and proof operations*) 
20333  92 
use "rule_insts.ML"; 
26609
53754d9ee31f
load thy_info.ML after outer_syntax.ML  avoids backpatching of load_thy;
wenzelm
parents:
26598
diff
changeset

93 
use "../Thy/thm_deps.ML"; 
16025  94 
use "find_theorems.ML"; 
5818
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

95 
use "isar_cmd.ML"; 
962bfe78a297
Isar  Intelligible SemiAutomated Reasoning for Isabelle.
wenzelm
parents:
diff
changeset

96 
use "isar_syn.ML"; 