Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
moved classical tools from theory IFOL to FOL;
authorwenzelm
Tue, 31 Jul 2007 21:19:18 +0200
changeset 24097 86734ba03ca2
parent 24096 74926cdbf071
child 24098 f1eb34ae33af
moved classical tools from theory IFOL to FOL;
src/FOL/FOL.thy file | annotate | diff | comparison | revisions
src/FOL/IFOL.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/FOL.thy	Tue Jul 31 19:40:28 2007 +0200
+++ b/src/FOL/FOL.thy	Tue Jul 31 21:19:18 2007 +0200
@@ -8,6 +8,9 @@
 theory FOL
 imports IFOL
 uses
+  "~~/src/Provers/classical.ML"
+  "~~/src/Provers/blast.ML"
+  "~~/src/Provers/clasimp.ML"
   ("cladata.ML")
   ("blastdata.ML")
   ("simpdata.ML")
--- a/src/FOL/IFOL.thy	Tue Jul 31 19:40:28 2007 +0200
+++ b/src/FOL/IFOL.thy	Tue Jul 31 21:19:18 2007 +0200
@@ -16,9 +16,6 @@
   "~~/src/Tools/IsaPlanner/rw_inst.ML"
   "~~/src/Provers/eqsubst.ML"
   "~~/src/Provers/induct_method.ML"
-  "~~/src/Provers/classical.ML"
-  "~~/src/Provers/blast.ML"
-  "~~/src/Provers/clasimp.ML"
   "~~/src/Provers/quantifier1.ML"
   "~~/src/Provers/project_rule.ML"
   ("fologic.ML")
isabelle