src/Sequents/ROOT.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21426 87ac12bed1ab
child 24106 f2965bf954dc
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
wenzelm@9000
     1
(*  Title:      Sequents/ROOT.ML
paulson@2073
     2
    ID:         $Id$
paulson@2073
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2073
     4
    Copyright   1991  University of Cambridge
paulson@2073
     5
wenzelm@17481
     6
Classical Sequent Calculus based on Pure Isabelle. 
paulson@2073
     7
*)
paulson@2073
     8
paulson@2073
     9
val banner = "Sequent Calculii";
paulson@2073
    10
writeln banner;
paulson@2073
    11
paulson@7120
    12
Unify.trace_bound:= 20;
paulson@7120
    13
Unify.search_bound := 40;
paulson@7120
    14
paulson@2073
    15
use_thy "LK";
wenzelm@21426
    16
paulson@2073
    17
use_thy "ILL";
wenzelm@21426
    18
use_thy "ILL_predlog";
wenzelm@21426
    19
use_thy "Washing";
wenzelm@21426
    20
paulson@2073
    21
use_thy "Modal0";
paulson@2073
    22
use_thy"T";
paulson@2073
    23
use_thy"S4";
paulson@2073
    24
use_thy"S43";