--- 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# ";
+