author  wenzelm 
Mon, 15 Dec 1997 14:40:13 +0100  
changeset 4410  b68047c56fce 
parent 4408  ad74412ef7a0 
child 4484  220ccae8a590 
permissions  rwrr 
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"; 

4410  11 
val version = "Isabelle98: January 1998"; 
0  12 

13 
print_depth 1; 

14 

15 
use "library.ML"; 

4278  16 
use "seq.ML"; 
1411  17 
use "symtab.ML"; 
3763  18 
use "name_space.ML"; 
0  19 
use "term.ML"; 
19  20 

21 
(*Syntax module*) 

2582  22 
cd "Syntax"; 
0  23 
use "ROOT.ML"; 
2582  24 
cd ".."; 
0  25 

4408  26 
(*Main system*) 
2960  27 
use "sorts.ML"; 
28 
use "type_infer.ML"; 

0  29 
use "type.ML"; 
30 
use "sign.ML"; 

31 
use "envir.ML"; 

32 
use "pattern.ML"; 

33 
use "unify.ML"; 

34 
use "net.ML"; 

35 
use "logic.ML"; 

1528  36 
use "theory.ML"; 
0  37 
use "thm.ML"; 
3986  38 
use "display.ML"; 
39 
use "pure_thy.ML"; 

1595  40 
use "deriv.ML"; 
0  41 
use "drule.ML"; 
42 
use "tctical.ML"; 

1582  43 
use "search.ML"; 
0  44 
use "tactic.ML"; 
45 
use "goals.ML"; 

403  46 
use "axclass.ML"; 
0  47 

618  48 
(*Theory parser and loader*) 
4408  49 
val global_names = ref false; (* FIXME tmp *) 
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 objectlogics 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; 