diff -r af364e2b4048 -r f2965bf954dc src/Sequents/ROOT.ML
--- a/src/Sequents/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
+++ b/src/Sequents/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
@@ -6,19 +6,7 @@
 Classical Sequent Calculus based on Pure Isabelle. 
 *)
 
-val banner = "Sequent Calculii";
-writeln banner;
-
 Unify.trace_bound:= 20;
 Unify.search_bound := 40;
 
-use_thy "LK";
-
-use_thy "ILL";
-use_thy "ILL_predlog";
-use_thy "Washing";
-
-use_thy "Modal0";
-use_thy"T";
-use_thy"S4";
-use_thy"S43";
+use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"];