author  wenzelm 
Tue, 20 Oct 1998 16:25:14 +0200  
changeset 5684  9a3acc4c7c2e 
parent 5607  5db9e2343ade 
child 5834  c6fea8488ce7 
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 

5684  15 
(*fake hiding of private structures*) 
16 
structure Hidden = struct end; 

4949  17 

5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset

18 
(*basic tools*) 
0  19 
use "library.ML"; 
5017
786a17461ab9
moved table.ML, object.ML, seq.ML, name_space.ML to General;
wenzelm
parents:
5004
diff
changeset

20 
cd "General"; use "ROOT.ML"; cd ".."; 
0  21 
use "term.ML"; 
19  22 

4949  23 
(*inner syntax module*) 
2582  24 
cd "Syntax"; 
0  25 
use "ROOT.ML"; 
2582  26 
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"; 
0  40 
use "thm.ML"; 
3986  41 
use "display.ML"; 
4781  42 
use "attribute.ML"; 
3986  43 
use "pure_thy.ML"; 
1595  44 
use "deriv.ML"; 
0  45 
use "drule.ML"; 
5244  46 
use "locale.ML"; 
0  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 

5211  58 
use "pure.ML"; 
59 

618  60 
use "install_pp.ML"; 
61 

5113  62 
(*if true then some packages won't be too serious about actually proving things*) 
5093  63 
val quick_and_dirty = ref false; 
64 

5568  65 
(*several objectlogics declare theories that hide basis library structures*) 
4209  66 
structure BasisLibrary = 
67 
struct 

5568  68 
structure List = List 
69 
and Option = Option 

5607  70 
and Bool = Bool 
71 
and Int = Int 

72 
and Real = Real; 

4209  73 
end; 
74 

75 
open Use; 

76 

3508  77 
print_depth 8; 