author | wenzelm |
Wed, 12 Nov 1997 16:20:49 +0100 | |
changeset 4209 | 4e0c98184285 |
parent 3986 | d788dcb86930 |
child 4256 | e768c42069bb |
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 |
||
19 | 6 |
Root file for Pure Isabelle: all modules in proper order for loading. |
4209 | 7 |
Loads Pure Isabelle into an empty ML database (see also IsaMakefile). |
0 | 8 |
*) |
9 |
||
10 |
val banner = "Pure Isabelle"; |
|
3280 | 11 |
val version = "Isabelle-94 revision 8: May 1997"; |
0 | 12 |
|
13 |
print_depth 1; |
|
14 |
||
15 |
use "library.ML"; |
|
1411 | 16 |
use "symtab.ML"; |
3763 | 17 |
use "name_space.ML"; |
0 | 18 |
use "term.ML"; |
19 | 19 |
|
20 |
(*Syntax module*) |
|
2582 | 21 |
cd "Syntax"; |
0 | 22 |
use "ROOT.ML"; |
2582 | 23 |
cd ".."; |
0 | 24 |
|
4209 | 25 |
(*Core system*) |
2960 | 26 |
use "sorts.ML"; |
27 |
use "type_infer.ML"; |
|
0 | 28 |
use "type.ML"; |
3864 | 29 |
use "data.ML"; |
0 | 30 |
use "sign.ML"; |
31 |
use "sequence.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"; |
0 | 38 |
use "thm.ML"; |
3986 | 39 |
use "display.ML"; |
40 |
use "pure_thy.ML"; |
|
1595 | 41 |
use "deriv.ML"; |
0 | 42 |
use "drule.ML"; |
43 |
use "tctical.ML"; |
|
1582 | 44 |
use "search.ML"; |
0 | 45 |
use "tactic.ML"; |
46 |
use "goals.ML"; |
|
403 | 47 |
use "axclass.ML"; |
0 | 48 |
|
618 | 49 |
(*Theory parser and loader*) |
2582 | 50 |
cd "Thy"; |
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
51 |
use "ROOT.ML"; |
2582 | 52 |
cd ".."; |
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset
|
53 |
|
618 | 54 |
use "install_pp.ML"; |
55 |
||
4209 | 56 |
(*several object-logics declare theories named List or Option, hiding |
57 |
the eponymous basis library structures*) |
|
58 |
structure BasisLibrary = |
|
59 |
struct |
|
60 |
structure List = List and Option = Option; |
|
61 |
end; |
|
62 |
||
63 |
open Use; |
|
64 |
||
3508 | 65 |
print_depth 8; |