src/HOL/SAT.thy
changeset 32232 6c394343360f
parent 30549 d2d7874648bd
child 34120 f9920a3ddf50
     1.1 --- a/src/HOL/SAT.thy	Mon Jul 27 20:45:40 2009 +0200
     1.2 +++ b/src/HOL/SAT.thy	Mon Jul 27 23:17:40 2009 +0200
     1.3 @@ -25,12 +25,12 @@
     1.4    maxtime=60,
     1.5    satsolver="auto"]
     1.6  
     1.7 -ML {* structure sat = SATFunc(structure cnf = cnf); *}
     1.8 +ML {* structure sat = SATFunc(cnf) *}
     1.9  
    1.10 -method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
    1.11 +method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
    1.12    "SAT solver"
    1.13  
    1.14 -method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
    1.15 +method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
    1.16    "SAT solver (with definitional CNF)"
    1.17  
    1.18  end