src/HOL/SAT.thy
changeset 21588 cd0dc678a205
parent 17809 195045659c06
child 26521 f8c4e79db153
--- a/src/HOL/SAT.thy	Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/SAT.thy	Wed Nov 29 15:44:51 2006 +0100
@@ -17,7 +17,7 @@
 begin
 
 text {* \medskip Late package setup: default values for refute, see
-  also theory @{text Refute}. *}
+  also theory @{theory Refute}. *}
 
 refute_params
  ["itself"=1,
@@ -30,10 +30,10 @@
 
 ML {* structure sat = SATFunc(structure cnf = cnf); *}
 
-method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
+method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
   "SAT solver"
 
-method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
+method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
   "SAT solver (with definitional CNF)"
 
 end