src/FOL/ROOT.ML
author wenzelm
Mon, 20 Jun 2005 22:13:56 +0200
changeset 16483 ace3c2b95353
parent 16019 0e1405402d53
child 18482 ac8456b4080c
permissions -rw-r--r--
removed obsolete print_depth;
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
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
val banner = "First-Order Logic with Natural Deduction";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
writeln banner;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
6260
wenzelm
parents: 5310
diff changeset
    11
use "~~/src/Provers/splitter.ML";
wenzelm
parents: 5310
diff changeset
    12
use "~~/src/Provers/ind.ML";
wenzelm
parents: 5310
diff changeset
    13
use "~~/src/Provers/hypsubst.ML";
11674
c67d5ed31417 use "~~/src/Provers/induct_method.ML";
wenzelm
parents: 9888
diff changeset
    14
use "~~/src/Provers/induct_method.ML";
9157
998dd2fb5795 new file Provers/make_elim.ML
paulson
parents: 7576
diff changeset
    15
use "~~/src/Provers/make_elim.ML";
6260
wenzelm
parents: 5310
diff changeset
    16
use "~~/src/Provers/classical.ML";
wenzelm
parents: 5310
diff changeset
    17
use "~~/src/Provers/blast.ML";
wenzelm
parents: 5310
diff changeset
    18
use "~~/src/Provers/clasimp.ML";
wenzelm
parents: 5310
diff changeset
    19
use "~~/src/Provers/quantifier1.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2237
diff changeset
    21
use_thy "FOL";