src/Sequents/ROOT.ML
author paulson
Tue, 27 Jul 1999 19:02:43 +0200
changeset 7098 86583034aacf
parent 6349 f7750d816c21
child 7120 6d5923cecece
permissions -rw-r--r--
installation of simplifier and classical reasoner, better rules etc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     1
(*  Title:      Sequents/ROOT
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     2
    ID:         $Id$
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     5
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     6
Adds Classical Sequent Calculus to a database containing pure Isabelle. 
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     7
*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     8
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     9
val banner = "Sequent Calculii";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    10
writeln banner;
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    11
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    12
print_depth 1;  
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    13
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    14
use "~~/src/Provers/simplifier.ML";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    15
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    16
use_thy "Sequents";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    17
use "prover.ML";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    18
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    19
use_thy "LK";
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    20
use "simpdata.ML";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    21
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    22
use_thy "ILL";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    23
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    24
use "modal.ML";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    25
use_thy "Modal0";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    26
use_thy"T";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    27
use_thy"S4";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    28
use_thy"S43";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    29
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    30
print_depth 8;