src/Sequents/ROOT.ML
changeset 2073 fb0655539d05
child 2247 d388a38f7198
equal deleted inserted replaced
2072:6ac12b9478d5 2073:fb0655539d05
       
     1 (*  Title:      Sequents/ROOT
       
     2     ID:         $Id$
       
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
       
     4     Copyright   1991  University of Cambridge
       
     5 
       
     6 Adds Classical Sequent Calculus to a database containing pure Isabelle. 
       
     7 *)
       
     8 
       
     9 val banner = "Sequent Calculii";
       
    10 writeln banner;
       
    11 
       
    12 init_thy_reader();
       
    13 
       
    14 print_depth 1;  
       
    15 
       
    16 use_thy "Sequents";
       
    17 use "prover.ML";
       
    18 
       
    19 use_thy "LK";
       
    20 use_thy "ILL";
       
    21 
       
    22 use_thy "Modal0";
       
    23 use_thy"T";
       
    24 use_thy"S4";
       
    25 use_thy"S43";
       
    26 
       
    27 use "../Pure/install_pp.ML";
       
    28 print_depth 8;
       
    29 
       
    30 val Sequents_build_completed = ();    (*indicate successful build*)