author  wenzelm 
Fri, 21 May 2004 21:21:38 +0200  
changeset 14781  2be804d1dda9 
parent 13402  e6e826bb8c3c 
child 14823  ebb8499d0fd2 
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"; 

11835  10 
val version = "Isabelle repository version"; (*filled in automatically!*) 
11 

0  12 

12248  13 
print_depth 10; 
0  14 

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

6164  17 

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

4949  20 

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

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

23 
cd "General"; use "ROOT.ML"; cd ".."; 
14781  24 

25 
(*fundamental structures*) 

0  26 
use "term.ML"; 
14781  27 
use "sorts.ML"; 
28 
use "type.ML"; 

19  29 

4949  30 
(*inner syntax module*) 
6178  31 
cd "Syntax"; use "ROOT.ML"; cd ".."; 
0  32 

11966  33 
(*core system*) 
2960  34 
use "type_infer.ML"; 
0  35 
use "sign.ML"; 
36 
use "envir.ML"; 

37 
use "pattern.ML"; 

38 
use "unify.ML"; 

39 
use "net.ML"; 

40 
use "logic.ML"; 

1528  41 
use "theory.ML"; 
5004  42 
use "theory_data.ML"; 
6178  43 
use "context.ML"; 
11511  44 
use "proofterm.ML"; 
0  45 
use "thm.ML"; 
3986  46 
use "display.ML"; 
13271  47 
use "fact_index.ML"; 
3986  48 
use "pure_thy.ML"; 
0  49 
use "drule.ML"; 
10413  50 
use "meta_simplifier.ML"; 
0  51 
use "tctical.ML"; 
1582  52 
use "search.ML"; 
0  53 
use "tactic.ML"; 
54 

11511  55 
(*proof term operations*) 
11882  56 
cd "Proof"; use "ROOT.ML"; cd ".."; 
11511  57 

6178  58 
(*theory system operations*) 
59 
cd "Thy"; use "ROOT.ML"; cd ".."; 

73
075db6ac7f2f
delete_file now has type string > unit in both NJ and POLY,
clasohm
parents:
19
diff
changeset

60 

5834  61 
(*the Isar subsystem*) 
6178  62 
cd "Isar"; use "ROOT.ML"; cd ".."; 
5834  63 

6693
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset

64 
use "axclass.ML"; 
11511  65 
use "codegen.ML"; 
13402  66 
use "Proof/extraction.ML"; 
11511  67 

11966  68 
(*oldstyle goal package*) 
69 
use "goals.ML"; 

70 

12778
3120e338ffae
Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
12248
diff
changeset

71 
(*configuration for Proof General*) 
3120e338ffae
Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
12248
diff
changeset

72 
use "proof_general.ML"; 
6693
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset

73 

6178  74 
(*final Pure theory setup*) 
5211  75 
use "pure.ML"; 
76 

5568  77 
(*several objectlogics declare theories that hide basis library structures*) 
4209  78 
structure BasisLibrary = 
79 
struct 

6178  80 
structure List = List; 
81 
structure Option = Option; 

82 
structure Bool = Bool; 

83 
structure String = String; 

84 
structure Int = Int; 

85 
structure Real = Real; 

4209  86 
end; 
87 

6178  88 
use "install_pp.ML"; 
6226  89 

6237  90 
val use = ThyInfo.use; 
6226  91 
val cd = File.cd o Path.unpack; 
92 

7938  93 
ml_prompts "ML> " "ML# "; 
11511  94 

11545  95 
proofs := 0; 