--- a/src/HOL/Refute.thy Wed Apr 02 15:58:43 2008 +0200
+++ b/src/HOL/Refute.thy Wed Apr 02 15:58:57 2008 +0200
@@ -9,11 +9,12 @@
header {* Refute *}
theory Refute
-imports Datatype
-uses "Tools/prop_logic.ML"
- "Tools/sat_solver.ML"
- "Tools/refute.ML"
- "Tools/refute_isar.ML"
+imports Inductive
+uses
+ "Tools/prop_logic.ML"
+ "Tools/sat_solver.ML"
+ "Tools/refute.ML"
+ "Tools/refute_isar.ML"
begin
setup Refute.setup
--- a/src/HOL/SAT.thy Wed Apr 02 15:58:43 2008 +0200
+++ b/src/HOL/SAT.thy Wed Apr 02 15:58:57 2008 +0200
@@ -8,12 +8,11 @@
header {* Reconstructing external resolution proofs for propositional logic *}
-theory SAT imports Refute
-
+theory SAT
+imports Refute
uses
- "Tools/cnf_funcs.ML"
- "Tools/sat_funcs.ML"
-
+ "Tools/cnf_funcs.ML"
+ "Tools/sat_funcs.ML"
begin
text {* \medskip Late package setup: default values for refute, see
@@ -27,7 +26,6 @@
maxtime=60,
satsolver="auto"]
-
ML {* structure sat = SATFunc(structure cnf = cnf); *}
method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}