src/Sequents/ROOT.ML
changeset 2073 fb0655539d05
child 2247 d388a38f7198
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Sequents/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
     1.3 @@ -0,0 +1,30 @@
     1.4 +(*  Title:      Sequents/ROOT
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +Adds Classical Sequent Calculus to a database containing pure Isabelle. 
    1.10 +*)
    1.11 +
    1.12 +val banner = "Sequent Calculii";
    1.13 +writeln banner;
    1.14 +
    1.15 +init_thy_reader();
    1.16 +
    1.17 +print_depth 1;  
    1.18 +
    1.19 +use_thy "Sequents";
    1.20 +use "prover.ML";
    1.21 +
    1.22 +use_thy "LK";
    1.23 +use_thy "ILL";
    1.24 +
    1.25 +use_thy "Modal0";
    1.26 +use_thy"T";
    1.27 +use_thy"S4";
    1.28 +use_thy"S43";
    1.29 +
    1.30 +use "../Pure/install_pp.ML";
    1.31 +print_depth 8;
    1.32 +
    1.33 +val Sequents_build_completed = ();    (*indicate successful build*)