src/HOL/SAT.thy
changeset 21588 cd0dc678a205
parent 17809 195045659c06
child 26521 f8c4e79db153
     1.1 --- a/src/HOL/SAT.thy	Wed Nov 29 15:44:46 2006 +0100
     1.2 +++ b/src/HOL/SAT.thy	Wed Nov 29 15:44:51 2006 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  begin
     1.5  
     1.6  text {* \medskip Late package setup: default values for refute, see
     1.7 -  also theory @{text Refute}. *}
     1.8 +  also theory @{theory Refute}. *}
     1.9  
    1.10  refute_params
    1.11   ["itself"=1,
    1.12 @@ -30,10 +30,10 @@
    1.13  
    1.14  ML {* structure sat = SATFunc(structure cnf = cnf); *}
    1.15  
    1.16 -method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
    1.17 +method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
    1.18    "SAT solver"
    1.19  
    1.20 -method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
    1.21 +method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
    1.22    "SAT solver (with definitional CNF)"
    1.23  
    1.24  end