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 +