7 val version = "Isabelle repository version"; (*filled in automatically!*)
9 (*if true then some tools will OMIT some proofs*)
10 val quick_and_dirty = ref false;
15 use "General/basics.ML";
18 cd "General"; use "ROOT.ML"; cd "..";
20 (*fundamental structures*)
25 use "General/pretty.ML";
26 use "Syntax/lexicon.ML";
27 use "Syntax/simple_syntax.ML";
35 (*inner syntax module*)
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";
45 use "ML/ml_syntax.ML";
47 (*core of tactical proof system*)
50 use "primitive_defs.ML";
57 use "interpretation.ML";
71 use "meta_simplifier.ML";
77 (*proof term operations*)
78 use "Proof/reconstruct.ML";
79 use "Proof/proof_syntax.ML";
80 use "Proof/proof_rewrite_rules.ML";
81 use "Proof/proofchecker.ML";
83 (*the main Isar system*)
84 cd "Isar"; use "ROOT.ML"; cd "..";
87 use "Proof/extraction.ML";
89 cd "Tools"; use "ROOT.ML"; cd "..";
93 (*configuration for Proof General*)
94 cd "ProofGeneral"; use "ROOT.ML"; cd "..";