src/FOL/ROOT.ML
author wenzelm
Fri Apr 27 16:31:20 2007 +0200 (2007-04-27)
changeset 22822 c1a6a2159e69
parent 21539 c5cf9243ad62
child 23157 340586b2305c
permissions -rw-r--r--
removed obsolete induct/simp tactic;
wenzelm@7355
     1
(*  Title:      FOL/ROOT.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
*)
clasohm@0
     6
clasohm@0
     7
val banner = "First-Order Logic with Natural Deduction";
clasohm@0
     8
clasohm@0
     9
writeln banner;
clasohm@0
    10
wenzelm@6260
    11
use "~~/src/Provers/splitter.ML";
wenzelm@6260
    12
use "~~/src/Provers/hypsubst.ML";
dixon@19835
    13
use "~~/src/Provers/IsaPlanner/zipper.ML";
dixon@19835
    14
use "~~/src/Provers/IsaPlanner/isand.ML";
dixon@19835
    15
use "~~/src/Provers/IsaPlanner/rw_tools.ML";
dixon@19835
    16
use "~~/src/Provers/IsaPlanner/rw_inst.ML";
wenzelm@18595
    17
use "~~/src/Provers/eqsubst.ML";
wenzelm@11674
    18
use "~~/src/Provers/induct_method.ML";
wenzelm@6260
    19
use "~~/src/Provers/classical.ML";
wenzelm@6260
    20
use "~~/src/Provers/blast.ML";
wenzelm@6260
    21
use "~~/src/Provers/clasimp.ML";
wenzelm@6260
    22
use "~~/src/Provers/quantifier1.ML";
wenzelm@18482
    23
use "~~/src/Provers/project_rule.ML";
clasohm@0
    24
paulson@2469
    25
use_thy "FOL";
wenzelm@21539
    26
wenzelm@21539
    27
structure IFOL =
wenzelm@21539
    28
struct
wenzelm@21539
    29
  val thy = theory "IFOL";
wenzelm@21539
    30
end;
wenzelm@21539
    31
wenzelm@21539
    32
structure FOL =
wenzelm@21539
    33
struct
wenzelm@21539
    34
  val thy = theory "FOL";
wenzelm@21539
    35
end;