equal
deleted
inserted
replaced
6 Root file for Pure Isabelle: all modules in proper order for loading. |
6 Root file for Pure Isabelle: all modules in proper order for loading. |
7 Loads Pure Isabelle into an empty ML database (see also IsaMakefile). |
7 Loads Pure Isabelle into an empty ML database (see also IsaMakefile). |
8 *) |
8 *) |
9 |
9 |
10 val banner = "Pure Isabelle"; |
10 val banner = "Pure Isabelle"; |
11 val version = "Isabelle-94 revision 8: May 1997"; |
11 val version = "Isabelle98: Jan 1998"; |
12 |
12 |
13 print_depth 1; |
13 print_depth 1; |
14 |
14 |
15 use "library.ML"; |
15 use "library.ML"; |
16 use "seq.ML"; |
16 use "seq.ML"; |
21 (*Syntax module*) |
21 (*Syntax module*) |
22 cd "Syntax"; |
22 cd "Syntax"; |
23 use "ROOT.ML"; |
23 use "ROOT.ML"; |
24 cd ".."; |
24 cd ".."; |
25 |
25 |
26 (*Core system*) |
26 (*Main system*) |
27 use "sorts.ML"; |
27 use "sorts.ML"; |
28 use "type_infer.ML"; |
28 use "type_infer.ML"; |
29 use "type.ML"; |
29 use "type.ML"; |
30 use "sign.ML"; |
30 use "sign.ML"; |
31 use "envir.ML"; |
31 use "envir.ML"; |
44 use "tactic.ML"; |
44 use "tactic.ML"; |
45 use "goals.ML"; |
45 use "goals.ML"; |
46 use "axclass.ML"; |
46 use "axclass.ML"; |
47 |
47 |
48 (*Theory parser and loader*) |
48 (*Theory parser and loader*) |
49 |
49 val global_names = ref false; (* FIXME tmp *) |
50 (* FIXME tmp *) |
|
51 val global_names = ref false; |
|
52 |
|
53 cd "Thy"; |
50 cd "Thy"; |
54 use "ROOT.ML"; |
51 use "ROOT.ML"; |
55 cd ".."; |
52 cd ".."; |
56 |
53 |
57 use "install_pp.ML"; |
54 use "install_pp.ML"; |