src/FOL/ROOT.ML
author wenzelm
Thu, 07 Sep 2000 20:48:51 +0200
changeset 9888 c5622848bf18
parent 9157 998dd2fb5795
child 11674 c67d5ed31417
permissions -rw-r--r--
added Provers/rulify.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6349
diff changeset
     1
(*  Title:      FOL/ROOT.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1356
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6349
diff changeset
     6
First-Order Logic.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
val banner = "First-Order Logic with Natural Deduction";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
writeln banner;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
print_depth 1;  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
6260
wenzelm
parents: 5310
diff changeset
    15
use "~~/src/Provers/simplifier.ML";
wenzelm
parents: 5310
diff changeset
    16
use "~~/src/Provers/splitter.ML";
wenzelm
parents: 5310
diff changeset
    17
use "~~/src/Provers/ind.ML";
wenzelm
parents: 5310
diff changeset
    18
use "~~/src/Provers/hypsubst.ML";
9888
c5622848bf18 added Provers/rulify.ML;
wenzelm
parents: 9157
diff changeset
    19
use "~~/src/Provers/rulify.ML";
9157
998dd2fb5795 new file Provers/make_elim.ML
paulson
parents: 7576
diff changeset
    20
use "~~/src/Provers/make_elim.ML";
6260
wenzelm
parents: 5310
diff changeset
    21
use "~~/src/Provers/classical.ML";
wenzelm
parents: 5310
diff changeset
    22
use "~~/src/Provers/blast.ML";
wenzelm
parents: 5310
diff changeset
    23
use "~~/src/Provers/clasimp.ML";
wenzelm
parents: 5310
diff changeset
    24
use "~~/src/Provers/quantifier1.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2237
diff changeset
    26
use_thy "FOL";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
print_depth 8;