src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Thu Aug 30 22:51:11 2001 +0200
+++ b/src/Pure/ROOT.ML	Fri Aug 31 16:06:21 2001 +0200
@@ -7,7 +7,7 @@
 *)
 
 val banner = "Pure Isabelle";
-val version = "Isabelle repository version";    (*filled in automatically!*)
+val version = "Isabelle repository";
 
 print_depth 1;
 
@@ -38,10 +38,10 @@
 use "theory.ML";
 use "theory_data.ML";
 use "context.ML";
+use "proofterm.ML";
 use "thm.ML";
 use "display.ML";
 use "pure_thy.ML";
-use "deriv.ML";
 use "drule.ML";
 use "meta_simplifier.ML";
 use "locale.ML";
@@ -50,6 +50,14 @@
 use "tactic.ML";
 use "goals.ML";
 
+(*proof term operations*)
+cd "Proof";
+use "reconstruct.ML";
+use "proof_syntax.ML";
+use "proof_rewrite_rules.ML";
+use "proofchecker.ML";
+cd "..";
+
 (*theory system operations*)
 cd "Thy"; use "ROOT.ML"; cd "..";
 
@@ -58,6 +66,9 @@
 
 use "axclass.ML";
 
+(*code generator*)
+use "codegen.ML";
+
 (*external interfaces*)
 cd "Interface"; use "ROOT.ML"; cd "..";
 
@@ -82,3 +93,4 @@
 
 print_depth 8;
 ml_prompts "ML> " "ML# ";
+