moved classical tools from theory IFOL to FOL;
authorwenzelm
Tue Jul 31 21:19:18 2007 +0200 (2007-07-31)
changeset 2409786734ba03ca2
parent 24096 74926cdbf071
child 24098 f1eb34ae33af
moved classical tools from theory IFOL to FOL;
src/FOL/FOL.thy
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/FOL.thy	Tue Jul 31 19:40:28 2007 +0200
     1.2 +++ b/src/FOL/FOL.thy	Tue Jul 31 21:19:18 2007 +0200
     1.3 @@ -8,6 +8,9 @@
     1.4  theory FOL
     1.5  imports IFOL
     1.6  uses
     1.7 +  "~~/src/Provers/classical.ML"
     1.8 +  "~~/src/Provers/blast.ML"
     1.9 +  "~~/src/Provers/clasimp.ML"
    1.10    ("cladata.ML")
    1.11    ("blastdata.ML")
    1.12    ("simpdata.ML")
     2.1 --- a/src/FOL/IFOL.thy	Tue Jul 31 19:40:28 2007 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Tue Jul 31 21:19:18 2007 +0200
     2.3 @@ -16,9 +16,6 @@
     2.4    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     2.5    "~~/src/Provers/eqsubst.ML"
     2.6    "~~/src/Provers/induct_method.ML"
     2.7 -  "~~/src/Provers/classical.ML"
     2.8 -  "~~/src/Provers/blast.ML"
     2.9 -  "~~/src/Provers/clasimp.ML"
    2.10    "~~/src/Provers/quantifier1.ML"
    2.11    "~~/src/Provers/project_rule.ML"
    2.12    ("fologic.ML")