author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 5834 | c6fea8488ce7 |
child 6038 | dfdb7584cf96 |
permissions | -rw-r--r-- |
19 | 1 |
(* Title: Pure/ROOT.ML |
0 | 2 |
ID: $Id$ |
19 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
4986 | 6 |
Root file for Pure Isabelle. |
0 | 7 |
*) |
8 |
||
9 |
val banner = "Pure Isabelle"; |
|
4986 | 10 |
val version = "Isabelle repository"; |
0 | 11 |
|
12 |
print_depth 1; |
|
13 |
||
5684 | 14 |
(*fake hiding of private structures*) |
15 |
structure Hidden = struct end; |
|
4949 | 16 |
|
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset
|
17 |
(*basic tools*) |
0 | 18 |
use "library.ML"; |
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset
|
19 |
cd "General"; use "ROOT.ML"; cd ".."; |
0 | 20 |
use "term.ML"; |
19 | 21 |
|
4949 | 22 |
(*inner syntax module*) |
2582 | 23 |
cd "Syntax"; |
0 | 24 |
use "ROOT.ML"; |
2582 | 25 |
cd ".."; |
0 | 26 |
|
4949 | 27 |
(*main system*) |
2960 | 28 |
use "sorts.ML"; |
29 |
use "type_infer.ML"; |
|
0 | 30 |
use "type.ML"; |
31 |
use "sign.ML"; |
|
32 |
use "envir.ML"; |
|
33 |
use "pattern.ML"; |
|
34 |
use "unify.ML"; |
|
35 |
use "net.ML"; |
|
36 |
use "logic.ML"; |
|
1528 | 37 |
use "theory.ML"; |
5004 | 38 |
use "theory_data.ML"; |
5834 | 39 |
use "object_logic.ML"; |
0 | 40 |
use "thm.ML"; |
3986 | 41 |
use "display.ML"; |
4781 | 42 |
use "attribute.ML"; |
3986 | 43 |
use "pure_thy.ML"; |
1595 | 44 |
use "deriv.ML"; |
0 | 45 |
use "drule.ML"; |
5244 | 46 |
use "locale.ML"; |
0 | 47 |
use "tctical.ML"; |
1582 | 48 |
use "search.ML"; |
0 | 49 |
use "tactic.ML"; |
50 |
use "goals.ML"; |
|
403 | 51 |
use "axclass.ML"; |
0 | 52 |
|
4949 | 53 |
(*theory parser and loader*) |
2582 | 54 |
cd "Thy"; |
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
55 |
use "ROOT.ML"; |
2582 | 56 |
cd ".."; |
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
57 |
|
5834 | 58 |
(*the Isar subsystem*) |
59 |
cd "Isar"; |
|
60 |
use "ROOT.ML"; |
|
61 |
cd ".."; |
|
62 |
||
5211 | 63 |
use "pure.ML"; |
64 |
||
618 | 65 |
use "install_pp.ML"; |
66 |
||
5113 | 67 |
(*if true then some packages won't be too serious about actually proving things*) |
5093 | 68 |
val quick_and_dirty = ref false; |
69 |
||
5568 | 70 |
(*several object-logics declare theories that hide basis library structures*) |
4209 | 71 |
structure BasisLibrary = |
72 |
struct |
|
5568 | 73 |
structure List = List |
74 |
and Option = Option |
|
5607 | 75 |
and Bool = Bool |
76 |
and Int = Int |
|
77 |
and Real = Real; |
|
4209 | 78 |
end; |
79 |
||
80 |
open Use; |
|
81 |
||
3508 | 82 |
print_depth 8; |
5834 | 83 |
(*ml_prompts "ML> " "ML# ";*) |