author | wenzelm |
Mon, 08 Jun 1998 15:57:50 +0200 | |
changeset 5004 | cf4e3b487caf |
parent 4991 | d7d525466221 |
child 5017 | 786a17461ab9 |
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; |
|
4978 | 13 |
ml_prompts "> " "# "; |
0 | 14 |
|
4949 | 15 |
|
16 |
(*basic utils*) |
|
0 | 17 |
use "library.ML"; |
4484 | 18 |
use "table.ML"; |
4991 | 19 |
use "object.ML"; |
4278 | 20 |
use "seq.ML"; |
3763 | 21 |
use "name_space.ML"; |
0 | 22 |
use "term.ML"; |
19 | 23 |
|
4949 | 24 |
(*inner syntax module*) |
2582 | 25 |
cd "Syntax"; |
0 | 26 |
use "ROOT.ML"; |
2582 | 27 |
cd ".."; |
0 | 28 |
|
4949 | 29 |
(*main system*) |
2960 | 30 |
use "sorts.ML"; |
31 |
use "type_infer.ML"; |
|
0 | 32 |
use "type.ML"; |
33 |
use "sign.ML"; |
|
34 |
use "envir.ML"; |
|
35 |
use "pattern.ML"; |
|
36 |
use "unify.ML"; |
|
37 |
use "net.ML"; |
|
38 |
use "logic.ML"; |
|
1528 | 39 |
use "theory.ML"; |
5004 | 40 |
use "theory_data.ML"; |
0 | 41 |
use "thm.ML"; |
3986 | 42 |
use "display.ML"; |
4781 | 43 |
use "attribute.ML"; |
3986 | 44 |
use "pure_thy.ML"; |
1595 | 45 |
use "deriv.ML"; |
0 | 46 |
use "drule.ML"; |
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 |
|
618 | 58 |
use "install_pp.ML"; |
59 |
||
4209 | 60 |
(*several object-logics declare theories named List or Option, hiding |
61 |
the eponymous basis library structures*) |
|
62 |
structure BasisLibrary = |
|
63 |
struct |
|
64 |
structure List = List and Option = Option; |
|
65 |
end; |
|
66 |
||
67 |
open Use; |
|
68 |
||
3508 | 69 |
print_depth 8; |