src/FOL/ROOT.ML
author paulson
Fri, 29 Oct 2004 15:16:02 +0200
changeset 15270 8b3f707a78a7
parent 11771 b7b100a2de1d
child 16019 0e1405402d53
permissions -rw-r--r--
fixed reference to renamed theorem
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
print_depth 1;  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
6260
wenzelm
parents: 5310
diff changeset
    13
use "~~/src/Provers/simplifier.ML";
wenzelm
parents: 5310
diff changeset
    14
use "~~/src/Provers/splitter.ML";
wenzelm
parents: 5310
diff changeset
    15
use "~~/src/Provers/ind.ML";
wenzelm
parents: 5310
diff changeset
    16
use "~~/src/Provers/hypsubst.ML";
11674
c67d5ed31417 use "~~/src/Provers/induct_method.ML";
wenzelm
parents: 9888
diff changeset
    17
use "~~/src/Provers/induct_method.ML";
9157
998dd2fb5795 new file Provers/make_elim.ML
paulson
parents: 7576
diff changeset
    18
use "~~/src/Provers/make_elim.ML";
6260
wenzelm
parents: 5310
diff changeset
    19
use "~~/src/Provers/classical.ML";
wenzelm
parents: 5310
diff changeset
    20
use "~~/src/Provers/blast.ML";
wenzelm
parents: 5310
diff changeset
    21
use "~~/src/Provers/clasimp.ML";
wenzelm
parents: 5310
diff changeset
    22
use "~~/src/Provers/quantifier1.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2237
diff changeset
    24
use_thy "FOL";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
print_depth 8;