src/Sequents/ROOT.ML
author wenzelm
Wed Jul 09 17:00:34 1997 +0200 (1997-07-09)
changeset 3511 da4dd8b7ced4
parent 2247 d388a38f7198
child 3948 3428c0a88449
permissions -rw-r--r--
removed obsolete init_pps and init_thy_reader;
     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 print_depth 1;  
    13 
    14 use_thy "Sequents";
    15 use "prover.ML";
    16 
    17 use_thy "LK";
    18 use_thy "ILL";
    19 
    20 use_thy "Modal0";
    21 use_thy"T";
    22 use_thy"S4";
    23 use_thy"S43";
    24 
    25 print_depth 8;
    26 
    27 val Sequents_build_completed = ();    (*indicate successful build*)