1.1 --- a/src/Pure/ROOT.ML	Thu Aug 30 22:51:11 2001 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Aug 31 16:06:21 2001 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  *)
     1.5  
     1.6  val banner = "Pure Isabelle";
     1.7 -val version = "Isabelle repository version";    (*filled in automatically!*)
     1.8 +val version = "Isabelle repository";
     1.9  
    1.10  print_depth 1;
    1.11  
    1.12 @@ -38,10 +38,10 @@
    1.13  use "theory.ML";
    1.14  use "theory_data.ML";
    1.15  use "context.ML";
    1.16 +use "proofterm.ML";
    1.17  use "thm.ML";
    1.18  use "display.ML";
    1.19  use "pure_thy.ML";
    1.20 -use "deriv.ML";
    1.21  use "drule.ML";
    1.22  use "meta_simplifier.ML";
    1.23  use "locale.ML";
    1.24 @@ -50,6 +50,14 @@
    1.25  use "tactic.ML";
    1.26  use "goals.ML";
    1.27  
    1.28 +(*proof term operations*)
    1.29 +cd "Proof";
    1.30 +use "reconstruct.ML";
    1.31 +use "proof_syntax.ML";
    1.32 +use "proof_rewrite_rules.ML";
    1.33 +use "proofchecker.ML";
    1.34 +cd "..";
    1.35 +
    1.36  (*theory system operations*)
    1.37  cd "Thy"; use "ROOT.ML"; cd "..";
    1.38  
    1.39 @@ -58,6 +66,9 @@
    1.40  
    1.41  use "axclass.ML";
    1.42  
    1.43 +(*code generator*)
    1.44 +use "codegen.ML";
    1.45 +
    1.46  (*external interfaces*)
    1.47  cd "Interface"; use "ROOT.ML"; cd "..";
    1.48  
    1.49 @@ -82,3 +93,4 @@
    1.50  
    1.51  print_depth 8;
    1.52  ml_prompts "ML> " "ML# ";
    1.53 +