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) *}