--- a/src/Sequents/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ROOT.ML Sun Sep 18 15:20:08 2005 +0200
@@ -3,29 +3,18 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Adds Classical Sequent Calculus to a database containing pure Isabelle.
+Classical Sequent Calculus based on Pure Isabelle.
*)
val banner = "Sequent Calculii";
writeln banner;
-print_depth 1;
-
Unify.trace_bound:= 20;
Unify.search_bound := 40;
-use_thy "Sequents";
-use "prover.ML";
-
use_thy "LK";
-use "simpdata.ML";
-
use_thy "ILL";
-
-use "modal.ML";
use_thy "Modal0";
use_thy"T";
use_thy"S4";
use_thy"S43";
-
-print_depth 8;