src/Sequents/ROOT.ML
author wenzelm
Tue, 30 May 2000 16:08:38 +0200
changeset 9000 c20d58286a51
parent 7120 6d5923cecece
child 16019 0e1405402d53
permissions -rw-r--r--
cleaned up;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9000
c20d58286a51 cleaned up;
wenzelm
parents: 7120
diff changeset
     1
(*  Title:      Sequents/ROOT.ML
2073
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
7120
6d5923cecece sequents require higher bounds
paulson
parents: 7098
diff changeset
    14
Unify.trace_bound:= 20;
6d5923cecece sequents require higher bounds
paulson
parents: 7098
diff changeset
    15
Unify.search_bound := 40;
6d5923cecece sequents require higher bounds
paulson
parents: 7098
diff changeset
    16
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    17
use "~~/src/Provers/simplifier.ML";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    18
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    19
use_thy "Sequents";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    20
use "prover.ML";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    21
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    22
use_thy "LK";
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    23
use "simpdata.ML";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    24
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    25
use_thy "ILL";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    26
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6349
diff changeset
    27
use "modal.ML";
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    28
use_thy "Modal0";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    29
use_thy"T";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    30
use_thy"S4";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    31
use_thy"S43";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    32
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    33
print_depth 8;