src/HOL/SAT.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 32232 6c394343360f
     1.1 --- a/src/HOL/SAT.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/SAT.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/SAT.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Alwen Tiu, Tjark Weber
     1.7      Copyright   2005
     1.8  
     1.9 @@ -28,10 +27,10 @@
    1.10  
    1.11  ML {* structure sat = SATFunc(structure cnf = cnf); *}
    1.12  
    1.13 -method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
    1.14 +method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
    1.15    "SAT solver"
    1.16  
    1.17 -method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
    1.18 +method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
    1.19    "SAT solver (with definitional CNF)"
    1.20  
    1.21  end