author  wenzelm 
Sun, 29 Jan 2006 19:23:44 +0100  
changeset 18837  577438cc653e 
parent 18169  45def66f86cb 
child 18870  020e242c02a0 
permissions  rwrr 
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 cyclefree 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 metasimplifier with the Proverssimplifier. 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"; 
13402  82 
use "Proof/extraction.ML"; 
11511  83 

15481  84 
(*the IsaPlanner subsystem*) 
85 
cd "IsaPlanner"; use "ROOT.ML"; cd ".."; 

86 

17467  87 
cd "Tools"; use "ROOT.ML"; cd ".."; 
88 

12778
3120e338ffae
Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
12248
diff
changeset

89 
(*configuration for Proof General*) 
17467  90 
setmp proofs 1 use "proof_general.ML"; 
16781  91 

15801  92 
use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end; 
18837  93 

94 
Context.add_setup 

95 
(Theory.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> 

96 
Theory.add_syntax Syntax.applC_syntax); 

15801  97 
use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end; 
98 

17467  99 
(*final ML setup*) 
6178  100 
use "install_pp.ML"; 
6237  101 
val use = ThyInfo.use; 
6226  102 
val cd = File.cd o Path.unpack; 
7938  103 
ml_prompts "ML> " "ML# "; 
11511  104 

11545  105 
proofs := 0; 