author  wenzelm 
Sat, 14 Apr 2007 17:36:06 +0200  
changeset 22679  68cd69a388e2 
parent 22592  97b5290a8c34 
child 22694  077ce0e019fa 
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 

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 nonsense*) 

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

4949  33 
(*inner syntax module*) 
22679  34 
use "Syntax/lexicon.ML"; 
35 
use "Syntax/ast.ML"; 

36 
use "Syntax/syn_ext.ML"; 

37 
use "Syntax/parser.ML"; 

38 
use "Syntax/type_ext.ML"; 

39 
use "Syntax/syn_trans.ML"; 

40 
use "Syntax/mixfix.ML"; 

41 
use "Syntax/printer.ML"; 

42 
use "Syntax/syntax.ML"; 

43 
structure Hidden = struct end; 

44 
structure Lexicon = Hidden; 

45 
structure Ast = Hidden; 

46 
structure SynExt = Hidden; 

47 
structure Parser = Hidden; 

48 
structure TypeExt = Hidden; 

49 
structure SynTrans = Hidden; 

50 
structure Mixfix = Hidden; 

51 
structure Printer = Hidden; 

52 

53 
use "type_infer.ML"; 

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 cyclefree 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 metasimplifier with the Proverssimplifier. 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 

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

105 
Theory.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; 