author  oheimb 
Fri, 29 Jan 1999 17:10:26 +0100  
changeset 6164  a0e9501d56f8 
parent 6083  ede76e7af057 
child 6178  d6d6bdfe8340 
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; 

13 

6164  14 
(* global flags *) 
15 
val print_mode = ref ([]:string list); 

16 
(*if true then some packages will OMIT SOME PROOFS*) 

17 
val quick_and_dirty = ref false; 

18 

5684  19 
(*fake hiding of private structures*) 
20 
structure Hidden = struct end; 

4949  21 

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

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

24 
cd "General"; use "ROOT.ML"; cd ".."; 
0  25 
use "term.ML"; 
19  26 

4949  27 
(*inner syntax module*) 
2582  28 
cd "Syntax"; 
0  29 
use "ROOT.ML"; 
2582  30 
cd ".."; 
0  31 

4949  32 
(*main system*) 
2960  33 
use "sorts.ML"; 
34 
use "type_infer.ML"; 

0  35 
use "type.ML"; 
36 
use "sign.ML"; 

37 
use "envir.ML"; 

38 
use "pattern.ML"; 

39 
use "unify.ML"; 

40 
use "net.ML"; 

41 
use "logic.ML"; 

1528  42 
use "theory.ML"; 
5004  43 
use "theory_data.ML"; 
5834  44 
use "object_logic.ML"; 
0  45 
use "thm.ML"; 
3986  46 
use "display.ML"; 
47 
use "pure_thy.ML"; 

1595  48 
use "deriv.ML"; 
0  49 
use "drule.ML"; 
5244  50 
use "locale.ML"; 
0  51 
use "tctical.ML"; 
1582  52 
use "search.ML"; 
0  53 
use "tactic.ML"; 
54 
use "goals.ML"; 

403  55 
use "axclass.ML"; 
0  56 

4949  57 
(*theory parser and loader*) 
2582  58 
cd "Thy"; 
73
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

59 
use "ROOT.ML"; 
2582  60 
cd ".."; 
73
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

61 

5834  62 
(*the Isar subsystem*) 
63 
cd "Isar"; 

64 
use "ROOT.ML"; 

65 
cd ".."; 

66 

5211  67 
use "pure.ML"; 
68 

618  69 
use "install_pp.ML"; 
70 

5568  71 
(*several objectlogics declare theories that hide basis library structures*) 
4209  72 
structure BasisLibrary = 
73 
struct 

5568  74 
structure List = List 
75 
and Option = Option 

5607  76 
and Bool = Bool 
6038  77 
and String = String 
5607  78 
and Int = Int 
79 
and Real = Real; 

4209  80 
end; 
81 

82 
open Use; 

83 

3508  84 
print_depth 8; 
5834  85 
(*ml_prompts "ML> " "ML# ";*) 