author | wenzelm |
Wed, 02 Nov 2005 14:46:54 +0100 | |
changeset 18059 | ce6cff74931b |
parent 17963 | 5574f676092c |
child 18169 | 45def66f86cb |
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 |
||
17474
e4cdb9f061fb
added quick_and_dirty (from Isar/skip_proofs.ML);
wenzelm
parents:
17467
diff
changeset
|
10 |
(*if true then some tools will OMIT some proofs*) |
e4cdb9f061fb
added quick_and_dirty (from Isar/skip_proofs.ML);
wenzelm
parents:
17467
diff
changeset
|
11 |
val quick_and_dirty = ref false; |
0 | 12 |
|
12248 | 13 |
print_depth 10; |
0 | 14 |
|
5684 | 15 |
(*fake hiding of private structures*) |
16 |
structure Hidden = struct end; |
|
4949 | 17 |
|
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset
|
18 |
(*basic tools*) |
0 | 19 |
use "library.ML"; |
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset
|
20 |
cd "General"; use "ROOT.ML"; cd ".."; |
14781 | 21 |
|
22 |
(*fundamental structures*) |
|
0 | 23 |
use "term.ML"; |
14823
ebb8499d0fd2
moved print_mode to General/output.ML; load General/pretty.ML early;
wenzelm
parents:
14781
diff
changeset
|
24 |
use "General/pretty.ML"; |
14781 | 25 |
use "sorts.ML"; |
26 |
use "type.ML"; |
|
16435 | 27 |
use "context.ML"; |
16980 | 28 |
use "compress.ML"; |
19 | 29 |
|
4949 | 30 |
(*inner syntax module*) |
6178 | 31 |
cd "Syntax"; use "ROOT.ML"; cd ".."; |
0 | 32 |
|
15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
33 |
(*core of tactical proof system*) |
2960 | 34 |
use "type_infer.ML"; |
18059 | 35 |
use "consts.ML"; |
0 | 36 |
use "sign.ML"; |
37 |
use "envir.ML"; |
|
38 |
use "pattern.ML"; |
|
39 |
use "unify.ML"; |
|
40 |
use "net.ML"; |
|
41 |
use "logic.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
|
42 |
use "defs.ML"; |
1528 | 43 |
use "theory.ML"; |
11511 | 44 |
use "proofterm.ML"; |
0 | 45 |
use "thm.ML"; |
3986 | 46 |
use "display.ML"; |
13271 | 47 |
use "fact_index.ML"; |
3986 | 48 |
use "pure_thy.ML"; |
0 | 49 |
use "drule.ML"; |
50 |
use "tctical.ML"; |
|
1582 | 51 |
use "search.ML"; |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
14823
diff
changeset
|
52 |
use "meta_simplifier.ML"; |
17963 | 53 |
use "goal.ML"; |
0 | 54 |
use "tactic.ML"; |
55 |
||
11511 | 56 |
(*proof term operations*) |
15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
57 |
use "Proof/reconstruct.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
58 |
use "Proof/proof_syntax.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
59 |
use "Proof/proof_rewrite_rules.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
60 |
use "Proof/proofchecker.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
61 |
|
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
62 |
(*theory auto loader database*) |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
63 |
use "Thy/thy_load.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
64 |
use "Thy/thy_info.ML"; |
11511 | 65 |
|
15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
66 |
(*theory syntax -- new format*) |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
67 |
use "Isar/outer_lex.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
68 |
|
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
69 |
(*theory presentation*) |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
70 |
use "Thy/html.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
71 |
use "Thy/latex.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
72 |
use "Thy/present.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
73 |
use "Thy/thm_deps.ML"; |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
74 |
|
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
75 |
(*theorem database ML interface*) |
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset
|
76 |
use "Thy/thm_database.ML"; |
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
77 |
|
16435 | 78 |
(*the Isar system*) |
6178 | 79 |
cd "Isar"; use "ROOT.ML"; cd ".."; |
5834 | 80 |
|
6693
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset
|
81 |
use "axclass.ML"; |
11511 | 82 |
use "codegen.ML"; |
13402 | 83 |
use "Proof/extraction.ML"; |
11511 | 84 |
|
15481 | 85 |
(*the IsaPlanner subsystem*) |
86 |
cd "IsaPlanner"; use "ROOT.ML"; cd ".."; |
|
87 |
||
17467 | 88 |
cd "Tools"; use "ROOT.ML"; cd ".."; |
89 |
||
12778
3120e338ffae
Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
12248
diff
changeset
|
90 |
(*configuration for Proof General*) |
17467 | 91 |
setmp proofs 1 use "proof_general.ML"; |
16781 | 92 |
|
15801 | 93 |
use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end; |
94 |
use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end; |
|
95 |
||
17467 | 96 |
(*final ML setup*) |
6178 | 97 |
use "install_pp.ML"; |
6237 | 98 |
val use = ThyInfo.use; |
6226 | 99 |
val cd = File.cd o Path.unpack; |
7938 | 100 |
ml_prompts "ML> " "ML# "; |
11511 | 101 |
|
11545 | 102 |
proofs := 0; |