--- 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"];