src/Sequents/ROOT.ML
author paulson
Wed, 09 Oct 1996 13:32:33 +0200
changeset 2073 fb0655539d05
child 2247 d388a38f7198
permissions -rw-r--r--
New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)

(*  Title:      Sequents/ROOT
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Adds Classical Sequent Calculus to a database containing pure Isabelle. 
*)

val banner = "Sequent Calculii";
writeln banner;

init_thy_reader();

print_depth 1;  

use_thy "Sequents";
use "prover.ML";

use_thy "LK";
use_thy "ILL";

use_thy "Modal0";
use_thy"T";
use_thy"S4";
use_thy"S43";

use "../Pure/install_pp.ML";
print_depth 8;

val Sequents_build_completed = ();    (*indicate successful build*)