equal
deleted
inserted
replaced
14 "Tools/cnf_funcs.ML" |
14 "Tools/cnf_funcs.ML" |
15 "Tools/sat_funcs.ML" |
15 "Tools/sat_funcs.ML" |
16 |
16 |
17 begin |
17 begin |
18 |
18 |
|
19 (* |
19 ML {* structure sat = SATFunc(structure cnf_struct = cnf); *} |
20 ML {* structure sat = SATFunc(structure cnf_struct = cnf); *} |
20 |
21 |
21 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *} |
22 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *} |
22 "SAT solver" |
23 "SAT solver" |
23 |
24 |
24 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *} |
25 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *} |
25 "SAT solver (with definitional CNF)" |
26 "SAT solver (with definitional CNF)" |
26 |
27 |
27 (* |
28 |
28 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *} |
29 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *} |
29 "Transforming hypotheses in a goal into CNF" |
30 "Transforming hypotheses in a goal into CNF" |
30 |
31 |
31 method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *} |
32 method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *} |
32 "Transforming the conclusion of a goal to CNF" |
33 "Transforming the conclusion of a goal to CNF" |