src/HOL/SAT.thy
changeset 26521 f8c4e79db153
parent 21588 cd0dc678a205
child 30510 4120fc59dd85
     1.1 --- a/src/HOL/SAT.thy	Wed Apr 02 15:58:43 2008 +0200
     1.2 +++ b/src/HOL/SAT.thy	Wed Apr 02 15:58:57 2008 +0200
     1.3 @@ -8,12 +8,11 @@
     1.4  
     1.5  header {* Reconstructing external resolution proofs for propositional logic *}
     1.6  
     1.7 -theory SAT imports Refute
     1.8 -
     1.9 +theory SAT
    1.10 +imports Refute
    1.11  uses
    1.12 -     "Tools/cnf_funcs.ML"
    1.13 -     "Tools/sat_funcs.ML"
    1.14 -
    1.15 +  "Tools/cnf_funcs.ML"
    1.16 +  "Tools/sat_funcs.ML"
    1.17  begin
    1.18  
    1.19  text {* \medskip Late package setup: default values for refute, see
    1.20 @@ -27,7 +26,6 @@
    1.21    maxtime=60,
    1.22    satsolver="auto"]
    1.23  
    1.24 -
    1.25  ML {* structure sat = SATFunc(structure cnf = cnf); *}
    1.26  
    1.27  method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}