--- a/src/HOL/SAT.thy Sat Sep 24 13:26:40 2005 +0200
+++ b/src/HOL/SAT.thy Sat Sep 24 13:54:35 2005 +0200
@@ -3,7 +3,7 @@
Author: Alwen Tiu, Tjark Weber
Copyright 2005
-Basic setup for the 'sat' tactic.
+Basic setup for the 'sat' and 'satx' tactic.
*)
header {* Reconstructing external resolution proofs for propositional logic *}
@@ -16,8 +16,7 @@
begin
-(*
-ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
+ML {* structure sat = SATFunc(structure cnf = cnf); *}
method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
"SAT solver"
@@ -25,7 +24,7 @@
method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
"SAT solver (with definitional CNF)"
-
+(*
method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
"Transforming hypotheses in a goal into CNF"