src/FOL/ROOT.ML
changeset 23157 340586b2305c
parent 22822 c1a6a2159e69
child 23161 cd928fd965a8
     1.1 --- a/src/FOL/ROOT.ML	Thu May 31 14:34:07 2007 +0200
     1.2 +++ b/src/FOL/ROOT.ML	Thu May 31 14:34:09 2007 +0200
     1.3 @@ -5,31 +5,6 @@
     1.4  *)
     1.5  
     1.6  val banner = "First-Order Logic with Natural Deduction";
     1.7 -
     1.8  writeln banner;
     1.9  
    1.10 -use "~~/src/Provers/splitter.ML";
    1.11 -use "~~/src/Provers/hypsubst.ML";
    1.12 -use "~~/src/Provers/IsaPlanner/zipper.ML";
    1.13 -use "~~/src/Provers/IsaPlanner/isand.ML";
    1.14 -use "~~/src/Provers/IsaPlanner/rw_tools.ML";
    1.15 -use "~~/src/Provers/IsaPlanner/rw_inst.ML";
    1.16 -use "~~/src/Provers/eqsubst.ML";
    1.17 -use "~~/src/Provers/induct_method.ML";
    1.18 -use "~~/src/Provers/classical.ML";
    1.19 -use "~~/src/Provers/blast.ML";
    1.20 -use "~~/src/Provers/clasimp.ML";
    1.21 -use "~~/src/Provers/quantifier1.ML";
    1.22 -use "~~/src/Provers/project_rule.ML";
    1.23 -
    1.24  use_thy "FOL";
    1.25 -
    1.26 -structure IFOL =
    1.27 -struct
    1.28 -  val thy = theory "IFOL";
    1.29 -end;
    1.30 -
    1.31 -structure FOL =
    1.32 -struct
    1.33 -  val thy = theory "FOL";
    1.34 -end;