author  wenzelm 
Mon, 08 Jun 1998 15:57:50 +0200  
changeset 5004  cf4e3b487caf 
parent 4991  d7d525466221 
child 5017  786a17461ab9 
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 

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 objectlogics 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; 