author | wenzelm |
Thu, 26 Apr 2007 12:00:05 +0200 | |
changeset 22796 | 34c316d7b630 |
parent 22694 | 077ce0e019fa |
child 22904 | de2d630e1548 |
permissions | -rw-r--r-- |
19 | 1 |
(* Title: Pure/ROOT.ML |
0 | 2 |
ID: $Id$ |
3 |
||
16842 | 4 |
Pure Isabelle. |
0 | 5 |
*) |
6 |
||
7 |
val banner = "Pure Isabelle"; |
|
11835 | 8 |
val version = "Isabelle repository version"; (*filled in automatically!*) |
9 |
||
12248 | 10 |
print_depth 10; |
0 | 11 |
|
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset
|
12 |
(*basic tools*) |
21396 | 13 |
use "General/basics.ML"; |
0 | 14 |
use "library.ML"; |
22592 | 15 |
|
16 |
(*generic non-sense*) |
|
17 |
val quick_and_dirty = ref false; |
|
18 |
val print_mode = ref ([]: string list); |
|
19 |
fun print_mode_active s = member (op =) (! print_mode) s; |
|
20 |
||
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset
|
21 |
cd "General"; use "ROOT.ML"; cd ".."; |
14781 | 22 |
|
23 |
(*fundamental structures*) |
|
20075 | 24 |
use "name.ML"; |
0 | 25 |
use "term.ML"; |
20507 | 26 |
use "term_subst.ML"; |
14823
ebb8499d0fd2
moved print_mode to General/output.ML; load General/pretty.ML early;
wenzelm
parents:
14781
diff
changeset
|
27 |
use "General/pretty.ML"; |
14781 | 28 |
use "sorts.ML"; |
29 |
use "type.ML"; |
|
16435 | 30 |
use "context.ML"; |
16980 | 31 |
use "compress.ML"; |
22694 | 32 |
use "type_infer.ML"; |
19 | 33 |
|
4949 | 34 |
(*inner syntax module*) |
22679 | 35 |
use "Syntax/lexicon.ML"; |
36 |
use "Syntax/ast.ML"; |
|
37 |
use "Syntax/syn_ext.ML"; |
|
38 |
use "Syntax/parser.ML"; |
|
39 |
use "Syntax/type_ext.ML"; |
|
40 |
use "Syntax/syn_trans.ML"; |
|
41 |
use "Syntax/mixfix.ML"; |
|
42 |
use "Syntax/printer.ML"; |
|
43 |
use "Syntax/syntax.ML"; |
|
44 |
structure Hidden = struct end; |
|
45 |
structure Lexicon = Hidden; |
|
46 |
structure Ast = Hidden; |
|
47 |
structure SynExt = Hidden; |
|
48 |
structure Parser = Hidden; |
|
49 |
structure TypeExt = Hidden; |
|
50 |
structure SynTrans = Hidden; |
|
51 |
structure Mixfix = Hidden; |
|
52 |
structure Printer = Hidden; |
|
53 |
||
21475 | 54 |
use "General/ml_syntax.ML"; |
0 | 55 |
|
15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
56 |
(*core of tactical proof system*) |
18934 | 57 |
use "envir.ML"; |
58 |
use "logic.ML"; |
|
18059 | 59 |
use "consts.ML"; |
0 | 60 |
use "sign.ML"; |
61 |
use "pattern.ML"; |
|
62 |
use "unify.ML"; |
|
63 |
use "net.ML"; |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
15825
diff
changeset
|
64 |
use "defs.ML"; |
1528 | 65 |
use "theory.ML"; |
11511 | 66 |
use "proofterm.ML"; |
0 | 67 |
use "thm.ML"; |
22361 | 68 |
use "more_thm.ML"; |
13271 | 69 |
use "fact_index.ML"; |
3986 | 70 |
use "pure_thy.ML"; |
19589 | 71 |
use "display.ML"; |
0 | 72 |
use "drule.ML"; |
22233 | 73 |
use "morphism.ML"; |
19898 | 74 |
use "variable.ML"; |
0 | 75 |
use "tctical.ML"; |
1582 | 76 |
use "search.ML"; |
21708 | 77 |
use "tactic.ML"; |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
14823
diff
changeset
|
78 |
use "meta_simplifier.ML"; |
19417 | 79 |
use "conjunction.ML"; |
20225 | 80 |
use "assumption.ML"; |
17963 | 81 |
use "goal.ML"; |
0 | 82 |
|
11511 | 83 |
(*proof term operations*) |
15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
84 |
use "Proof/reconstruct.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
85 |
use "Proof/proof_syntax.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
86 |
use "Proof/proof_rewrite_rules.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
87 |
use "Proof/proofchecker.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
88 |
|
22108 | 89 |
(*the main Isar system*) |
6178 | 90 |
cd "Isar"; use "ROOT.ML"; cd ".."; |
20207 | 91 |
use "subgoal.ML"; |
5834 | 92 |
|
13402 | 93 |
use "Proof/extraction.ML"; |
11511 | 94 |
|
17467 | 95 |
cd "Tools"; use "ROOT.ML"; cd ".."; |
96 |
||
12778
3120e338ffae
Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
12248
diff
changeset
|
97 |
(*configuration for Proof General*) |
21941 | 98 |
cd "ProofGeneral"; use "ROOT.ML"; cd ".."; |
16781 | 99 |
|
18991
0ded3b842878
use proof_general.ML: setmp quick_and_dirty captures default value;
wenzelm
parents:
18934
diff
changeset
|
100 |
use_thy "Pure"; |
0ded3b842878
use proof_general.ML: setmp quick_and_dirty captures default value;
wenzelm
parents:
18934
diff
changeset
|
101 |
structure Pure = struct val thy = theory "Pure" end; |
18837 | 102 |
|
103 |
Context.add_setup |
|
22796 | 104 |
(Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> |
105 |
Sign.add_syntax Syntax.applC_syntax); |
|
18991
0ded3b842878
use proof_general.ML: setmp quick_and_dirty captures default value;
wenzelm
parents:
18934
diff
changeset
|
106 |
use_thy "CPure"; |
0ded3b842878
use proof_general.ML: setmp quick_and_dirty captures default value;
wenzelm
parents:
18934
diff
changeset
|
107 |
structure CPure = struct val thy = theory "CPure" end; |
15801 | 108 |
|
17467 | 109 |
(*final ML setup*) |
6178 | 110 |
use "install_pp.ML"; |
6237 | 111 |
val use = ThyInfo.use; |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21708
diff
changeset
|
112 |
val cd = File.cd o Path.explode; |
7938 | 113 |
ml_prompts "ML> " "ML# "; |
11511 | 114 |
|
11545 | 115 |
proofs := 0; |