src/FOL/ROOT.ML
author wenzelm
Fri, 27 Apr 2007 16:31:20 +0200
changeset 22822 c1a6a2159e69
parent 21539 c5cf9243ad62
child 23157 340586b2305c
permissions -rw-r--r--
removed obsolete induct/simp tactic;
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/hypsubst.ML";
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    13
use "~~/src/Provers/IsaPlanner/zipper.ML";
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    14
use "~~/src/Provers/IsaPlanner/isand.ML";
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    15
use "~~/src/Provers/IsaPlanner/rw_tools.ML";
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 18595
diff changeset
    16
use "~~/src/Provers/IsaPlanner/rw_inst.ML";
18595
a52907967bae simplified EqSubst setup;
wenzelm
parents: 18529
diff changeset
    17
use "~~/src/Provers/eqsubst.ML";
11674
c67d5ed31417 use "~~/src/Provers/induct_method.ML";
wenzelm
parents: 9888
diff changeset
    18
use "~~/src/Provers/induct_method.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";
18482
ac8456b4080c added Provers/project_rule.ML
wenzelm
parents: 16483
diff changeset
    23
use "~~/src/Provers/project_rule.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2237
diff changeset
    25
use_thy "FOL";
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    26
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    27
structure IFOL =
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    28
struct
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    29
  val thy = theory "IFOL";
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    30
end;
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    31
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    32
structure FOL =
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    33
struct
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    34
  val thy = theory "FOL";
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 19835
diff changeset
    35
end;