equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 val banner = "Pure Isabelle"; |
7 val banner = "Pure Isabelle"; |
8 val version = "Isabelle repository version"; (*filled in automatically!*) |
8 val version = "Isabelle repository version"; (*filled in automatically!*) |
9 |
9 |
|
10 (*if true then some tools will OMIT some proofs*) |
|
11 val quick_and_dirty = ref false; |
|
12 |
10 print_depth 10; |
13 print_depth 10; |
11 |
14 |
12 (*basic tools*) |
15 (*basic tools*) |
13 use "General/basics.ML"; |
16 use "General/basics.ML"; |
14 use "library.ML"; |
17 use "library.ML"; |
15 |
|
16 (*generic non-sense*) |
|
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 |
18 |
21 cd "General"; use "ROOT.ML"; cd ".."; |
19 cd "General"; use "ROOT.ML"; cd ".."; |
22 |
20 |
23 (*fundamental structures*) |
21 (*fundamental structures*) |
24 use "name.ML"; |
22 use "name.ML"; |
40 use "Syntax/type_ext.ML"; |
38 use "Syntax/type_ext.ML"; |
41 use "Syntax/syn_trans.ML"; |
39 use "Syntax/syn_trans.ML"; |
42 use "Syntax/mixfix.ML"; |
40 use "Syntax/mixfix.ML"; |
43 use "Syntax/printer.ML"; |
41 use "Syntax/printer.ML"; |
44 use "Syntax/syntax.ML"; |
42 use "Syntax/syntax.ML"; |
45 structure Hidden = struct end; |
|
46 structure Lexicon = Hidden; |
|
47 structure Ast = Hidden; |
|
48 structure SynExt = Hidden; |
|
49 structure Parser = Hidden; |
|
50 structure TypeExt = Hidden; |
|
51 structure SynTrans = Hidden; |
|
52 structure Mixfix = Hidden; |
|
53 structure Printer = Hidden; |
|
54 |
43 |
55 use "General/ml_syntax.ML"; |
44 use "General/ml_syntax.ML"; |
56 |
45 |
57 (*core of tactical proof system*) |
46 (*core of tactical proof system*) |
58 use "envir.ML"; |
47 use "envir.ML"; |
97 cd "Tools"; use "ROOT.ML"; cd ".."; |
86 cd "Tools"; use "ROOT.ML"; cd ".."; |
98 |
87 |
99 (*configuration for Proof General*) |
88 (*configuration for Proof General*) |
100 cd "ProofGeneral"; use "ROOT.ML"; cd ".."; |
89 cd "ProofGeneral"; use "ROOT.ML"; cd ".."; |
101 |
90 |
102 use_thy "Pure"; |
91 use "pure_setup.ML"; |
103 structure Pure = struct val thy = theory "Pure" end; |
|
104 |
|
105 Context.add_setup |
|
106 (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> |
|
107 Sign.add_syntax Syntax.applC_syntax); |
|
108 use_thy "CPure"; |
|
109 structure CPure = struct val thy = theory "CPure" end; |
|
110 |
|
111 (*final ML setup*) |
|
112 use "install_pp.ML"; |
|
113 val use = ThyInfo.use; |
|
114 val cd = File.cd o Path.explode; |
|
115 ml_prompts "ML> " "ML# "; |
|
116 |
|
117 proofs := 0; |
|