equal
deleted
inserted
replaced
11 imports Refute |
11 imports Refute |
12 uses |
12 uses |
13 "Tools/sat_funcs.ML" |
13 "Tools/sat_funcs.ML" |
14 begin |
14 begin |
15 |
15 |
16 text {* \medskip Late package setup: default values for refute, see |
|
17 also theory @{theory Refute}. *} |
|
18 |
|
19 refute_params |
|
20 ["itself"=1, |
|
21 minsize=1, |
|
22 maxsize=8, |
|
23 maxvars=10000, |
|
24 maxtime=60, |
|
25 satsolver="auto", |
|
26 no_assms="false"] |
|
27 |
|
28 ML {* structure sat = SATFunc(cnf) *} |
16 ML {* structure sat = SATFunc(cnf) *} |
29 |
17 |
30 method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} |
18 method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} |
31 "SAT solver" |
19 "SAT solver" |
32 |
20 |