author | berghofe |
Fri, 31 Aug 2001 16:06:21 +0200 | |
changeset 11511 | ec89f5cff390 |
parent 11065 | 0038c3bedd75 |
child 11545 | 0b56d9c90dcf |
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"; |
|
11511 | 10 |
val version = "Isabelle repository"; |
0 | 11 |
|
12 |
print_depth 1; |
|
13 |
||
6178 | 14 |
(*global flags*) |
15 |
val print_mode = ref ([]: string list); |
|
6164 | 16 |
|
5684 | 17 |
(*fake hiding of private structures*) |
18 |
structure Hidden = struct end; |
|
4949 | 19 |
|
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset
|
20 |
(*basic tools*) |
0 | 21 |
use "library.ML"; |
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 ".."; |
0 | 23 |
use "term.ML"; |
19 | 24 |
|
4949 | 25 |
(*inner syntax module*) |
6178 | 26 |
cd "Syntax"; use "ROOT.ML"; cd ".."; |
0 | 27 |
|
4949 | 28 |
(*main system*) |
2960 | 29 |
use "sorts.ML"; |
30 |
use "type_infer.ML"; |
|
0 | 31 |
use "type.ML"; |
32 |
use "sign.ML"; |
|
33 |
use "envir.ML"; |
|
34 |
use "pattern.ML"; |
|
35 |
use "unify.ML"; |
|
36 |
use "net.ML"; |
|
37 |
use "logic.ML"; |
|
1528 | 38 |
use "theory.ML"; |
5004 | 39 |
use "theory_data.ML"; |
6178 | 40 |
use "context.ML"; |
11511 | 41 |
use "proofterm.ML"; |
0 | 42 |
use "thm.ML"; |
3986 | 43 |
use "display.ML"; |
44 |
use "pure_thy.ML"; |
|
0 | 45 |
use "drule.ML"; |
10413 | 46 |
use "meta_simplifier.ML"; |
5244 | 47 |
use "locale.ML"; |
0 | 48 |
use "tctical.ML"; |
1582 | 49 |
use "search.ML"; |
0 | 50 |
use "tactic.ML"; |
51 |
use "goals.ML"; |
|
52 |
||
11511 | 53 |
(*proof term operations*) |
54 |
cd "Proof"; |
|
55 |
use "reconstruct.ML"; |
|
56 |
use "proof_syntax.ML"; |
|
57 |
use "proof_rewrite_rules.ML"; |
|
58 |
use "proofchecker.ML"; |
|
59 |
cd ".."; |
|
60 |
||
6178 | 61 |
(*theory system operations*) |
62 |
cd "Thy"; use "ROOT.ML"; cd ".."; |
|
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
63 |
|
5834 | 64 |
(*the Isar subsystem*) |
6178 | 65 |
cd "Isar"; use "ROOT.ML"; cd ".."; |
5834 | 66 |
|
6693
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset
|
67 |
use "axclass.ML"; |
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset
|
68 |
|
11511 | 69 |
(*code generator*) |
70 |
use "codegen.ML"; |
|
71 |
||
6693
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset
|
72 |
(*external interfaces*) |
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset
|
73 |
cd "Interface"; use "ROOT.ML"; cd ".."; |
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset
|
74 |
|
6178 | 75 |
(*final Pure theory setup*) |
5211 | 76 |
use "pure.ML"; |
77 |
||
5568 | 78 |
(*several object-logics declare theories that hide basis library structures*) |
4209 | 79 |
structure BasisLibrary = |
80 |
struct |
|
6178 | 81 |
structure List = List; |
82 |
structure Option = Option; |
|
83 |
structure Bool = Bool; |
|
84 |
structure String = String; |
|
85 |
structure Int = Int; |
|
86 |
structure Real = Real; |
|
4209 | 87 |
end; |
88 |
||
6178 | 89 |
use "install_pp.ML"; |
6226 | 90 |
|
6237 | 91 |
val use = ThyInfo.use; |
6226 | 92 |
val cd = File.cd o Path.unpack; |
93 |
||
3508 | 94 |
print_depth 8; |
7938 | 95 |
ml_prompts "ML> " "ML# "; |
11511 | 96 |