author  wenzelm 
Tue, 17 Mar 2009 14:12:06 +0100  
changeset 30559  e5987a7ac5df 
parent 30173  eabece26b89b 
child 30639  fe40d740d7c1 
permissions  rwrr 
19  1 
(* Title: Pure/ROOT.ML 
0  2 

16842  3 
Pure Isabelle. 
0  4 
*) 
5 

26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

6 
structure Distribution = (*filledin by makedist*) 
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

7 
struct 
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

8 
val version = "Isabelle repository version"; 
27642
c0db1220b071
structure Distribution: swapped default for is_official;
wenzelm
parents:
27546
diff
changeset

9 
val is_official = false; 
c0db1220b071
structure Distribution: swapped default for is_official;
wenzelm
parents:
27546
diff
changeset

10 
val changelog = ""; 
26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

11 
end; 
11835  12 

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

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

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

15 

12248  16 
print_depth 10; 
0  17 

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

18 
(*basic tools*) 
21396  19 
use "General/basics.ML"; 
0  20 
use "library.ML"; 
22592  21 

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

22 
cd "General"; use "ROOT.ML"; cd ".."; 
28200  23 
cd "Concurrent"; use "ROOT.ML"; cd ".."; 
28120  24 

14781  25 
(*fundamental structures*) 
20075  26 
use "name.ML"; 
0  27 
use "term.ML"; 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29263
diff
changeset

28 
use "term_ord.ML"; 
20507  29 
use "term_subst.ML"; 
29263  30 
use "old_term.ML"; 
24257  31 
use "logic.ML"; 
14823
ebb8499d0fd2
moved print_mode to General/output.ML; load General/pretty.ML early;
wenzelm
parents:
14781
diff
changeset

32 
use "General/pretty.ML"; 
28404  33 
use "context.ML"; 
34 
use "context_position.ML"; 

24235  35 
use "Syntax/lexicon.ML"; 
36 
use "Syntax/simple_syntax.ML"; 

24272  37 
use "sorts.ML"; 
38 
use "type.ML"; 

24113  39 
use "config.ML"; 
19  40 

4949  41 
(*inner syntax module*) 
22679  42 
use "Syntax/ast.ML"; 
43 
use "Syntax/syn_ext.ML"; 

44 
use "Syntax/parser.ML"; 

45 
use "Syntax/type_ext.ML"; 

46 
use "Syntax/syn_trans.ML"; 

47 
use "Syntax/mixfix.ML"; 

48 
use "Syntax/printer.ML"; 

49 
use "Syntax/syntax.ML"; 

50 

27262  51 
use "type_infer.ML"; 
24574  52 
use "ML/ml_syntax.ML"; 
0  53 

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

54 
(*core of tactical proof system*) 
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset

55 
use "net.ML"; 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset

56 
use "item_net.ML"; 
18934  57 
use "envir.ML"; 
18059  58 
use "consts.ML"; 
24257  59 
use "primitive_defs.ML"; 
27546  60 
use "defs.ML"; 
0  61 
use "sign.ML"; 
62 
use "pattern.ML"; 

63 
use "unify.ML"; 

1528  64 
use "theory.ML"; 
24664  65 
use "interpretation.ML"; 
11511  66 
use "proofterm.ML"; 
0  67 
use "thm.ML"; 
22361  68 
use "more_thm.ML"; 
26279  69 
use "facts.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"; 
24833  75 
use "conv.ML"; 
0  76 
use "tctical.ML"; 
1582  77 
use "search.ML"; 
21708  78 
use "tactic.ML"; 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
14823
diff
changeset

79 
use "meta_simplifier.ML"; 
19417  80 
use "conjunction.ML"; 
20225  81 
use "assumption.ML"; 
17963  82 
use "goal.ML"; 
24963  83 
use "axclass.ML"; 
0  84 

30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

85 
(*main Isar stuff*) 
6178  86 
cd "Isar"; use "ROOT.ML"; cd ".."; 
20207  87 
use "subgoal.ML"; 
5834  88 

13402  89 
use "Proof/extraction.ML"; 
11511  90 

30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

91 
(*Isabelle/Isar system*) 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

92 
use "System/session.ML"; 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

93 
use "System/isar.ML"; 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

94 
use "System/isabelle_process.ML"; 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

95 

eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

96 
(*additional tools*) 
17467  97 
cd "Tools"; use "ROOT.ML"; cd ".."; 
98 

24455  99 
use "codegen.ML"; 
100 

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

101 
(*configuration for Proof General*) 
21941  102 
cd "ProofGeneral"; use "ROOT.ML"; cd ".."; 
16781  103 

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

104 
use "pure_setup.ML"; 