author  wenzelm 
Thu, 24 Jan 2008 23:51:11 +0100  
changeset 25953  03937086b1fe 
parent 25750  4e796867ccb5 
child 26109  c69c3559355b 
permissions  rwrr 
19  1 
(* Title: Pure/ROOT.ML 
0  2 
ID: $Id$ 
3 

16842  4 
Pure Isabelle. 
0  5 
*) 
6 

11835  7 
val version = "Isabelle repository version"; (*filled in automatically!*) 
8 

23825
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

9 
(*if true then some tools will OMIT some proofs*) 
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

10 
val quick_and_dirty = ref false; 
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

11 

12248  12 
print_depth 10; 
0  13 

5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset

14 
(*basic tools*) 
21396  15 
use "General/basics.ML"; 
0  16 
use "library.ML"; 
22592  17 

5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset

18 
cd "General"; use "ROOT.ML"; cd ".."; 
14781  19 

20 
(*fundamental structures*) 

20075  21 
use "name.ML"; 
0  22 
use "term.ML"; 
20507  23 
use "term_subst.ML"; 
24257  24 
use "logic.ML"; 
14823
ebb8499d0fd2
moved print_mode to General/output.ML; load General/pretty.ML early;
wenzelm
parents:
14781
diff
changeset

25 
use "General/pretty.ML"; 
24235  26 
use "Syntax/lexicon.ML"; 
27 
use "Syntax/simple_syntax.ML"; 

16435  28 
use "context.ML"; 
24272  29 
use "sorts.ML"; 
30 
use "type.ML"; 

31 
use "type_infer.ML"; 

24113  32 
use "config.ML"; 
16980  33 
use "compress.ML"; 
19  34 

4949  35 
(*inner syntax module*) 
22679  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 

24574  45 
use "ML/ml_syntax.ML"; 
0  46 

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

47 
(*core of tactical proof system*) 
18934  48 
use "envir.ML"; 
18059  49 
use "consts.ML"; 
24257  50 
use "primitive_defs.ML"; 
0  51 
use "sign.ML"; 
52 
use "pattern.ML"; 

53 
use "unify.ML"; 

54 
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

55 
use "defs.ML"; 
1528  56 
use "theory.ML"; 
24664  57 
use "interpretation.ML"; 
11511  58 
use "proofterm.ML"; 
0  59 
use "thm.ML"; 
22361  60 
use "more_thm.ML"; 
13271  61 
use "fact_index.ML"; 
3986  62 
use "pure_thy.ML"; 
19589  63 
use "display.ML"; 
0  64 
use "drule.ML"; 
22233  65 
use "morphism.ML"; 
19898  66 
use "variable.ML"; 
24833  67 
use "conv.ML"; 
0  68 
use "tctical.ML"; 
1582  69 
use "search.ML"; 
21708  70 
use "tactic.ML"; 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
14823
diff
changeset

71 
use "meta_simplifier.ML"; 
19417  72 
use "conjunction.ML"; 
20225  73 
use "assumption.ML"; 
17963  74 
use "goal.ML"; 
24963  75 
use "axclass.ML"; 
0  76 

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

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

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

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

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

82 

22108  83 
(*the main Isar system*) 
6178  84 
cd "Isar"; use "ROOT.ML"; cd ".."; 
20207  85 
use "subgoal.ML"; 
5834  86 

13402  87 
use "Proof/extraction.ML"; 
11511  88 

17467  89 
cd "Tools"; use "ROOT.ML"; cd ".."; 
90 

24455  91 
use "codegen.ML"; 
92 

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

93 
(*configuration for Proof General*) 
21941  94 
cd "ProofGeneral"; use "ROOT.ML"; cd ".."; 
16781  95 

23825
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

96 
use "pure_setup.ML"; 