src/HOL/SAT.thy
changeset 26521 f8c4e79db153
parent 21588 cd0dc678a205
child 30510 4120fc59dd85
--- 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) *}