equal
deleted
inserted
replaced
12 keywords "refute" :: diag and "refute_params" :: thy_decl |
12 keywords "refute" :: diag and "refute_params" :: thy_decl |
13 uses "Tools/refute.ML" |
13 uses "Tools/refute.ML" |
14 begin |
14 begin |
15 |
15 |
16 setup Refute.setup |
16 setup Refute.setup |
|
17 |
|
18 refute_params |
|
19 [itself = 1, |
|
20 minsize = 1, |
|
21 maxsize = 8, |
|
22 maxvars = 10000, |
|
23 maxtime = 60, |
|
24 satsolver = auto, |
|
25 no_assms = false] |
17 |
26 |
18 text {* |
27 text {* |
19 \small |
28 \small |
20 \begin{verbatim} |
29 \begin{verbatim} |
21 (* ------------------------------------------------------------------------- *) |
30 (* ------------------------------------------------------------------------- *) |
78 (* "no_assms" bool If "true", assumptions in structured proofs are *) |
87 (* "no_assms" bool If "true", assumptions in structured proofs are *) |
79 (* not considered. *) |
88 (* not considered. *) |
80 (* "expect" string Expected result ("genuine", "potential", "none", or *) |
89 (* "expect" string Expected result ("genuine", "potential", "none", or *) |
81 (* "unknown"). *) |
90 (* "unknown"). *) |
82 (* *) |
91 (* *) |
83 (* See 'HOL/SAT.thy' for default values. *) |
|
84 (* *) |
|
85 (* The size of particular types can be specified in the form type=size *) |
92 (* The size of particular types can be specified in the form type=size *) |
86 (* (where 'type' is a string, and 'size' is an int). Examples: *) |
93 (* (where 'type' is a string, and 'size' is an int). Examples: *) |
87 (* "'a"=1 *) |
94 (* "'a"=1 *) |
88 (* "List.list"=2 *) |
95 (* "List.list"=2 *) |
89 (* ------------------------------------------------------------------------- *) |
96 (* ------------------------------------------------------------------------- *) |