--- a/src/HOL/SAT.thy Sat Sep 24 10:47:22 2005 +0200
+++ b/src/HOL/SAT.thy Sat Sep 24 13:11:05 2005 +0200
@@ -16,6 +16,7 @@
begin
+(*
ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
@@ -24,7 +25,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"