author  wenzelm 
Fri, 17 Jun 2005 18:33:20 +0200  
changeset 16435  3b17850023f1 
parent 16108  cf468b93a02e 
child 16781  663235466562 
permissions  rwrr 
19  1 
(* Title: Pure/ROOT.ML 
0  2 
ID: $Id$ 
19  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

4986  6 
Root file for Pure Isabelle. 
0  7 
*) 
8 

9 
val banner = "Pure Isabelle"; 

11835  10 
val version = "Isabelle repository version"; (*filled in automatically!*) 
11 

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"; 
19  28 

4949  29 
(*inner syntax module*) 
6178  30 
cd "Syntax"; use "ROOT.ML"; cd ".."; 
0  31 

15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

32 
(*core of tactical proof system*) 
2960  33 
use "type_infer.ML"; 
0  34 
use "sign.ML"; 
35 
use "envir.ML"; 

36 
use "pattern.ML"; 

37 
use "unify.ML"; 

38 
use "net.ML"; 

39 
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

40 
use "defs.ML"; 
1528  41 
use "theory.ML"; 
11511  42 
use "proofterm.ML"; 
0  43 
use "thm.ML"; 
3986  44 
use "display.ML"; 
13271  45 
use "fact_index.ML"; 
3986  46 
use "pure_thy.ML"; 
0  47 
use "drule.ML"; 
48 
use "tctical.ML"; 

1582  49 
use "search.ML"; 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
14823
diff
changeset

50 
use "meta_simplifier.ML"; 
0  51 
use "tactic.ML"; 
52 

11511  53 
(*proof term operations*) 
15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

54 
use "Proof/reconstruct.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

55 
use "Proof/proof_syntax.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

56 
use "Proof/proof_rewrite_rules.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

57 
use "Proof/proofchecker.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

58 

1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

59 
(*theory auto loader database*) 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

60 
use "Thy/thy_load.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

61 
use "Thy/thy_info.ML"; 
11511  62 

15825
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

63 
(*theory syntax  old format*) 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

64 
use "Thy/thy_scan.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

65 
use "Thy/thy_parse.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

66 
use "Thy/thy_syn.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

67 

1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

68 
(*theory syntax  new format*) 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

69 
use "Isar/outer_lex.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

70 

1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

71 
(*theory presentation*) 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

72 
use "Thy/html.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

73 
use "Thy/latex.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

74 
use "Thy/present.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

75 
use "Thy/thm_deps.ML"; 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

76 

1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

77 
(*theorem database ML interface*) 
1576f9d3ffae
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm
parents:
15801
diff
changeset

78 
use "Thy/thm_database.ML"; 
73
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

79 

16435  80 
(*the Isar system*) 
6178  81 
cd "Isar"; use "ROOT.ML"; cd ".."; 
5834  82 

6693
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset

83 
use "axclass.ML"; 
11511  84 
use "codegen.ML"; 
13402  85 
use "Proof/extraction.ML"; 
11511  86 

15801  87 
(*old goal package  obsolete*) 
11966  88 
use "goals.ML"; 
89 

15481  90 
(*the IsaPlanner subsystem*) 
91 
cd "IsaPlanner"; use "ROOT.ML"; cd ".."; 

92 

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

93 
(*configuration for Proof General*) 
3120e338ffae
Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
12248
diff
changeset

94 
use "proof_general.ML"; 
6693
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset

95 

15801  96 
(*the Pure theories*) 
97 
use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end; 

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

99 

5211  100 

5568  101 
(*several objectlogics declare theories that hide basis library structures*) 
4209  102 
structure BasisLibrary = 
103 
struct 

6178  104 
structure List = List; 
105 
structure Option = Option; 

106 
structure Bool = Bool; 

107 
structure String = String; 

108 
structure Int = Int; 

109 
structure Real = Real; 

4209  110 
end; 
111 

6178  112 
use "install_pp.ML"; 
6226  113 

6237  114 
val use = ThyInfo.use; 
6226  115 
val cd = File.cd o Path.unpack; 
116 

7938  117 
ml_prompts "ML> " "ML# "; 
11511  118 

11545  119 
proofs := 0; 