src/Sequents/ROOT.ML
author paulson
Wed Oct 09 13:32:33 1996 +0200 (1996-10-09)
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)
paulson@2073
     1
(*  Title:      Sequents/ROOT
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
paulson@2073
     6
Adds Classical Sequent Calculus to a database containing pure Isabelle. 
paulson@2073
     7
*)
paulson@2073
     8
paulson@2073
     9
val banner = "Sequent Calculii";
paulson@2073
    10
writeln banner;
paulson@2073
    11
paulson@2073
    12
init_thy_reader();
paulson@2073
    13
paulson@2073
    14
print_depth 1;  
paulson@2073
    15
paulson@2073
    16
use_thy "Sequents";
paulson@2073
    17
use "prover.ML";
paulson@2073
    18
paulson@2073
    19
use_thy "LK";
paulson@2073
    20
use_thy "ILL";
paulson@2073
    21
paulson@2073
    22
use_thy "Modal0";
paulson@2073
    23
use_thy"T";
paulson@2073
    24
use_thy"S4";
paulson@2073
    25
use_thy"S43";
paulson@2073
    26
paulson@2073
    27
use "../Pure/install_pp.ML";
paulson@2073
    28
print_depth 8;
paulson@2073
    29
paulson@2073
    30
val Sequents_build_completed = ();    (*indicate successful build*)