# HG changeset patch
# User haftmann
# Date 1207144737 -7200
# Node ID f8c4e79db153a0a48eb53af98412ca589962ad63
# Parent  9e7b7c478cb167f29cc244302b14b7454733a203
tuned imports

diff -r 9e7b7c478cb1 -r f8c4e79db153 src/HOL/Refute.thy
--- 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
diff -r 9e7b7c478cb1 -r f8c4e79db153 src/HOL/SAT.thy
--- 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) *}