src/FOL/ROOT.ML
author wenzelm
Tue, 13 Jun 2006 23:41:39 +0200
changeset 19876 11d447d5d68c
parent 19835 81d6dc597559
child 21539 c5cf9243ad62
permissions -rw-r--r--
tuned;
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";
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    14
use "~~/src/Provers/IsaPlanner/zipper.ML";
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    15
use "~~/src/Provers/IsaPlanner/isand.ML";
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    16
use "~~/src/Provers/IsaPlanner/rw_tools.ML";
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    17
use "~~/src/Provers/IsaPlanner/rw_inst.ML";
18595
a52907967bae simplified EqSubst setup;
wenzelm
parents: 18529
diff changeset
    18
use "~~/src/Provers/eqsubst.ML";
11674
c67d5ed31417 use "~~/src/Provers/induct_method.ML";
wenzelm
parents: 9888
diff changeset
    19
use "~~/src/Provers/induct_method.ML";
6260
wenzelm
parents: 5310
diff changeset
    20
use "~~/src/Provers/classical.ML";
wenzelm
parents: 5310
diff changeset
    21
use "~~/src/Provers/blast.ML";
wenzelm
parents: 5310
diff changeset
    22
use "~~/src/Provers/clasimp.ML";
wenzelm
parents: 5310
diff changeset
    23
use "~~/src/Provers/quantifier1.ML";
18482
ac8456b4080c added Provers/project_rule.ML
wenzelm
parents: 16483
diff changeset
    24
use "~~/src/Provers/project_rule.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";