src/Sequents/ROOT.ML
author wenzelm
Mon Nov 20 23:47:10 2006 +0100 (2006-11-20)
changeset 21426 87ac12bed1ab
parent 17481 75166ebb619b
child 24106 f2965bf954dc
permissions -rw-r--r--
converted legacy ML scripts;
     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 Classical Sequent Calculus based on Pure Isabelle. 
     7 *)
     8 
     9 val banner = "Sequent Calculii";
    10 writeln banner;
    11 
    12 Unify.trace_bound:= 20;
    13 Unify.search_bound := 40;
    14 
    15 use_thy "LK";
    16 
    17 use_thy "ILL";
    18 use_thy "ILL_predlog";
    19 use_thy "Washing";
    20 
    21 use_thy "Modal0";
    22 use_thy"T";
    23 use_thy"S4";
    24 use_thy"S43";