src/Cube/ROOT.ML
changeset 24106 f2965bf954dc
parent 17453 eccff680177d
child 35762 af3ff2ba4c54
--- a/src/Cube/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
+++ b/src/Cube/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
@@ -6,8 +6,4 @@
 The Lambda-Cube a la Barendregt.
 *)
 
-val banner = "Barendregt's Lambda-Cube";
-writeln banner;
-
-use_thy "Cube";
-use_thy "Example";
+use_thys ["Cube", "Example"];