src/Sequents/ROOT.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 7120 6d5923cecece
child 16019 0e1405402d53
permissions -rw-r--r--
cleaned up;
     1 (*  Title:      Sequents/ROOT.ML
     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 Unify.trace_bound:= 20;
    15 Unify.search_bound := 40;
    16 
    17 use "~~/src/Provers/simplifier.ML";
    18 
    19 use_thy "Sequents";
    20 use "prover.ML";
    21 
    22 use_thy "LK";
    23 use "simpdata.ML";
    24 
    25 use_thy "ILL";
    26 
    27 use "modal.ML";
    28 use_thy "Modal0";
    29 use_thy"T";
    30 use_thy"S4";
    31 use_thy"S43";
    32 
    33 print_depth 8;