src/Sequents/ROOT.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 16019 0e1405402d53
child 21426 87ac12bed1ab
permissions -rw-r--r--
converted to Isar theory format;
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";
paulson@2073
    16
use_thy "ILL";
paulson@2073
    17
use_thy "Modal0";
paulson@2073
    18
use_thy"T";
paulson@2073
    19
use_thy"S4";
paulson@2073
    20
use_thy"S43";