src/HOL/SAT.thy
changeset 17625 1539d18e3e9f
parent 17618 1330157e156a
child 17627 ff1923b1978b
--- 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"