--- a/src/Cube/ROOT.ML Wed Jul 09 16:54:17 1997 +0200
+++ b/src/Cube/ROOT.ML Wed Jul 09 17:00:34 1997 +0200
@@ -1,20 +1,18 @@
-(* Title: Cube/ROOT
+(* Title: Cube/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
-The Lambda-Cube a la Barendregt
+The Lambda-Cube a la Barendregt.
*)
val banner = "Barendregt's Lambda-Cube";
writeln banner;
-init_thy_reader();
+print_depth 1;
-print_depth 1;
use_thy "Cube";
-init_pps ();
print_depth 8;
val Cube_build_completed = (); (*indicate successful build*)