--- a/ROOT.ML Thu Jun 29 12:29:58 1995 +0200
+++ b/ROOT.ML Tue Oct 24 14:59:17 1995 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/ROOT.ML
+(* Title: Old_HOL/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
Adds Classical Higher-order Logic to a database containing Pure Isabelle.
-Should be executed in the subdirectory HOL.
+Should be executed in the subdirectory Old_HOL.
*)
val banner = "Higher-Order Logic";
@@ -18,7 +18,6 @@
use "thy_syntax.ML";
use_thy "HOL";
-use "../Provers/simplifier.ML";
use "../Provers/splitter.ML";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
@@ -86,4 +85,6 @@
init_pps ();
print_depth 8;
+make_chart (); (*make HTML chart*)
+
val HOL_build_completed = (); (*indicate successful build*)