src/Sequents/ROOT.ML
changeset 17481 75166ebb619b
parent 16019 0e1405402d53
child 21426 87ac12bed1ab
--- 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;