src/Sequents/ROOT.ML
changeset 17481 75166ebb619b
parent 16019 0e1405402d53
child 21426 87ac12bed1ab
     1.1 --- a/src/Sequents/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -3,29 +3,18 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -Adds Classical Sequent Calculus to a database containing pure Isabelle. 
     1.8 +Classical Sequent Calculus based on Pure Isabelle. 
     1.9  *)
    1.10  
    1.11  val banner = "Sequent Calculii";
    1.12  writeln banner;
    1.13  
    1.14 -print_depth 1;  
    1.15 -
    1.16  Unify.trace_bound:= 20;
    1.17  Unify.search_bound := 40;
    1.18  
    1.19 -use_thy "Sequents";
    1.20 -use "prover.ML";
    1.21 -
    1.22  use_thy "LK";
    1.23 -use "simpdata.ML";
    1.24 -
    1.25  use_thy "ILL";
    1.26 -
    1.27 -use "modal.ML";
    1.28  use_thy "Modal0";
    1.29  use_thy"T";
    1.30  use_thy"S4";
    1.31  use_thy"S43";
    1.32 -
    1.33 -print_depth 8;