src/Pure/ROOT.ML
changeset 6178 d6d6bdfe8340
parent 6164 a0e9501d56f8
child 6226 42c94393d39e
     1.1 --- a/src/Pure/ROOT.ML	Wed Feb 03 16:02:21 1999 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Feb 03 16:27:36 1999 +0100
     1.3 @@ -11,10 +11,9 @@
     1.4  
     1.5  print_depth 1;
     1.6  
     1.7 -(* global flags *)
     1.8 -val print_mode = ref ([]:string list);
     1.9 -(*if true then some packages will OMIT SOME PROOFS*)
    1.10 -val quick_and_dirty = ref false;
    1.11 +(*global flags*)
    1.12 +val print_mode = ref ([]: string list);
    1.13 +val quick_and_dirty = ref false;        (*if true then some packages will OMIT SOME PROOFS*)
    1.14  
    1.15  (*fake hiding of private structures*)
    1.16  structure Hidden = struct end;
    1.17 @@ -25,9 +24,7 @@
    1.18  use "term.ML";
    1.19  
    1.20  (*inner syntax module*)
    1.21 -cd "Syntax";
    1.22 -use "ROOT.ML";
    1.23 -cd "..";
    1.24 +cd "Syntax"; use "ROOT.ML"; cd "..";
    1.25  
    1.26  (*main system*)
    1.27  use "sorts.ML";
    1.28 @@ -41,6 +38,7 @@
    1.29  use "logic.ML";
    1.30  use "theory.ML";
    1.31  use "theory_data.ML";
    1.32 +use "context.ML";
    1.33  use "object_logic.ML";
    1.34  use "thm.ML";
    1.35  use "display.ML";
    1.36 @@ -54,32 +52,27 @@
    1.37  use "goals.ML";
    1.38  use "axclass.ML";
    1.39  
    1.40 -(*theory parser and loader*)
    1.41 -cd "Thy";
    1.42 -use "ROOT.ML";
    1.43 -cd "..";
    1.44 +(*theory system operations*)
    1.45 +cd "Thy"; use "ROOT.ML"; cd "..";
    1.46  
    1.47  (*the Isar subsystem*)
    1.48 -cd "Isar";
    1.49 -use "ROOT.ML";
    1.50 -cd "..";
    1.51 +cd "Isar"; use "ROOT.ML"; cd "..";
    1.52  
    1.53 +(*final Pure theory setup*)
    1.54  use "pure.ML";
    1.55  
    1.56 -use "install_pp.ML";
    1.57 -
    1.58  (*several object-logics declare theories that hide basis library structures*)
    1.59  structure BasisLibrary =
    1.60  struct
    1.61 -  structure List   = List 
    1.62 -  and       Option = Option
    1.63 -  and       Bool   = Bool
    1.64 -  and       String = String
    1.65 -  and       Int    = Int
    1.66 -  and       Real   = Real;
    1.67 +  structure List = List;
    1.68 +  structure Option = Option;
    1.69 +  structure Bool = Bool;
    1.70 +  structure String = String;
    1.71 +  structure Int = Int;
    1.72 +  structure Real = Real;
    1.73  end;
    1.74  
    1.75 -open Use;
    1.76 -
    1.77 +use "install_pp.ML";
    1.78 +open BasicUse;
    1.79  print_depth 8;
    1.80  (*ml_prompts "ML> " "ML# ";*)