author  berghofe 
Fri, 31 Aug 2001 16:06:21 +0200  
changeset 11511  ec89f5cff390 
parent 11065  0038c3bedd75 
child 11545  0b56d9c90dcf 
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"; 

11511  10 
val version = "Isabelle repository"; 
0  11 

12 
print_depth 1; 

13 

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

6164  16 

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

4949  19 

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

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

22 
cd "General"; use "ROOT.ML"; cd ".."; 
0  23 
use "term.ML"; 
19  24 

4949  25 
(*inner syntax module*) 
6178  26 
cd "Syntax"; use "ROOT.ML"; 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"; 
6178  40 
use "context.ML"; 
11511  41 
use "proofterm.ML"; 
0  42 
use "thm.ML"; 
3986  43 
use "display.ML"; 
44 
use "pure_thy.ML"; 

0  45 
use "drule.ML"; 
10413  46 
use "meta_simplifier.ML"; 
5244  47 
use "locale.ML"; 
0  48 
use "tctical.ML"; 
1582  49 
use "search.ML"; 
0  50 
use "tactic.ML"; 
51 
use "goals.ML"; 

52 

11511  53 
(*proof term operations*) 
54 
cd "Proof"; 

55 
use "reconstruct.ML"; 

56 
use "proof_syntax.ML"; 

57 
use "proof_rewrite_rules.ML"; 

58 
use "proofchecker.ML"; 

59 
cd ".."; 

60 

6178  61 
(*theory system operations*) 
62 
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

63 

5834  64 
(*the Isar subsystem*) 
6178  65 
cd "Isar"; use "ROOT.ML"; cd ".."; 
5834  66 

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

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

68 

11511  69 
(*code generator*) 
70 
use "codegen.ML"; 

71 

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

72 
(*external interfaces*) 
fec75b36a809
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
wenzelm
parents:
6365
diff
changeset

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

74 

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

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

6178  81 
structure List = List; 
82 
structure Option = Option; 

83 
structure Bool = Bool; 

84 
structure String = String; 

85 
structure Int = Int; 

86 
structure Real = Real; 

4209  87 
end; 
88 

6178  89 
use "install_pp.ML"; 
6226  90 

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

3508  94 
print_depth 8; 
7938  95 
ml_prompts "ML> " "ML# "; 
11511  96 