src/HOL/SAT.thy
changeset 30510 4120fc59dd85
parent 26521 f8c4e79db153
child 30549 d2d7874648bd
     1.1 --- a/src/HOL/SAT.thy	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/SAT.thy	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -28,10 +28,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 (SIMPLE_METHOD' sat.sat_tac) *}
     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 (SIMPLE_METHOD' sat.satx_tac) *}
    1.13    "SAT solver (with definitional CNF)"
    1.14  
    1.15  end