src/HOL/SAT.thy
changeset 17809 195045659c06
parent 17722 8e098e040c2e
child 21588 cd0dc678a205
     1.1 --- a/src/HOL/SAT.thy	Sat Oct 08 23:43:15 2005 +0200
     1.2 +++ b/src/HOL/SAT.thy	Sun Oct 09 17:06:03 2005 +0200
     1.3 @@ -30,10 +30,10 @@
     1.4  
     1.5  ML {* structure sat = SATFunc(structure cnf = cnf); *}
     1.6  
     1.7 -method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
     1.8 +method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
     1.9    "SAT solver"
    1.10  
    1.11 -method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    1.12 +method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
    1.13    "SAT solver (with definitional CNF)"
    1.14  
    1.15  end