author | blanchet |
Mon, 06 Dec 2010 11:41:24 +0100 | |
changeset 40983 | 07526f546680 |
parent 40977 | 9140c5950494 |
child 41087 | d7b5fd465198 |
permissions | -rw-r--r-- |
38988 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
2 |
Author: Philipp Meyer, TU Muenchen |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
4 |
|
40977 | 5 |
Minimization of fact list for Metis using external provers. |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
6 |
*) |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
7 |
|
38988 | 8 |
signature SLEDGEHAMMER_MINIMIZE = |
32525 | 9 |
sig |
38988 | 10 |
type locality = Sledgehammer_Filter.locality |
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38015
diff
changeset
|
11 |
type params = Sledgehammer.params |
35867 | 12 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
13 |
val minimize_facts : |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38745
diff
changeset
|
14 |
params -> int -> int -> Proof.state -> ((string * locality) * thm list) list |
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38745
diff
changeset
|
15 |
-> ((string * locality) * thm list) list option * string |
38996 | 16 |
val run_minimize : |
17 |
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit |
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
18 |
end; |
32525 | 19 |
|
38988 | 20 |
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
21 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
22 |
|
39496
a52a4e4399c1
got caught once again by SML's pattern maching (ctor vs. var)
blanchet
parents:
39491
diff
changeset
|
23 |
open ATP_Proof |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
24 |
open Sledgehammer_Util |
38988 | 25 |
open Sledgehammer_Filter |
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38015
diff
changeset
|
26 |
open Sledgehammer |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
27 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
28 |
(* wrapper for calling external prover *) |
31236 | 29 |
|
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
30 |
fun string_for_failure ATP_Proof.Unprovable = "Unprovable." |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
31 |
| string_for_failure ATP_Proof.TimedOut = "Timed out." |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
32 |
| string_for_failure ATP_Proof.Interrupted = "Interrupted." |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
33 |
| string_for_failure _ = "Error." |
31236 | 34 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
35 |
fun n_facts names = |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
36 |
let val n = length names in |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
37 |
string_of_int n ^ " fact" ^ plural_s n ^ |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
38 |
(if n > 0 then |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
39 |
": " ^ (names |> map fst |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
40 |
|> sort_distinct string_ord |> space_implode " ") |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
41 |
else |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
42 |
"") |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
43 |
end |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
44 |
|
40342
3154f63e2bda
don't be overly verbose in Sledgehammer's minimizer
blanchet
parents:
40341
diff
changeset
|
45 |
fun test_facts ({debug, overlord, provers, full_types, isar_proof, |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
46 |
isar_shrink_factor, ...} : params) (prover : prover) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
47 |
explicit_apply timeout i n state facts = |
31236 | 48 |
let |
38015 | 49 |
val _ = |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
50 |
Output.urgent_message ("Testing " ^ n_facts (map fst facts) ^ "...") |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
51 |
val params = |
40342
3154f63e2bda
don't be overly verbose in Sledgehammer's minimizer
blanchet
parents:
40341
diff
changeset
|
52 |
{blocking = true, debug = debug, verbose = false, overlord = overlord, |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39496
diff
changeset
|
53 |
provers = provers, full_types = full_types, |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39496
diff
changeset
|
54 |
explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
55 |
max_relevant = NONE, isar_proof = isar_proof, |
38998 | 56 |
isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
57 |
val facts = |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
58 |
facts |> maps (fn (n, ths) => ths |> map (Untranslated o pair n)) |
40069 | 59 |
val {goal, ...} = Proof.goal state |
40065 | 60 |
val problem = |
61 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
|
40983 | 62 |
facts = facts} |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
63 |
val result as {outcome, used_facts, ...} = prover params (K "") problem |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
64 |
in |
40977 | 65 |
Output.urgent_message |
66 |
(case outcome of |
|
67 |
SOME failure => string_for_failure failure |
|
68 |
| NONE => |
|
69 |
if length used_facts = length facts then "Found proof." |
|
70 |
else "Found proof with " ^ n_facts used_facts ^ "."); |
|
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
71 |
result |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
72 |
end |
31236 | 73 |
|
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
74 |
(* minimalization of facts *) |
31236 | 75 |
|
40977 | 76 |
(* The sublinear algorithm works well in almost all situations, except when the |
77 |
external prover cannot return the list of used facts and hence returns all |
|
78 |
facts as used. In that case, the binary algorithm is much more |
|
79 |
appropriate. We can usually detect that situation just by looking at the |
|
80 |
number of used facts reported by the prover. *) |
|
81 |
val binary_threshold = 50 |
|
82 |
||
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
83 |
fun filter_used_facts used = filter (member (op =) used o fst) |
38015 | 84 |
|
85 |
fun sublinear_minimize _ [] p = p |
|
86 |
| sublinear_minimize test (x :: xs) (seen, result) = |
|
87 |
case test (xs @ seen) of |
|
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
88 |
result as {outcome = NONE, used_facts, ...} : prover_result => |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
89 |
sublinear_minimize test (filter_used_facts used_facts xs) |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
90 |
(filter_used_facts used_facts seen, result) |
38015 | 91 |
| _ => sublinear_minimize test xs (x :: seen, result) |
92 |
||
40977 | 93 |
fun binary_minimize test xs = |
94 |
let |
|
95 |
fun p xs = #outcome (test xs : prover_result) = NONE |
|
96 |
fun split [] p = p |
|
97 |
| split [h] (l, r) = (h :: l, r) |
|
98 |
| split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r) |
|
99 |
fun min _ [] = raise Empty |
|
100 |
| min _ [s0] = [s0] |
|
101 |
| min sup xs = |
|
102 |
let val (l0, r0) = split xs ([], []) in |
|
103 |
if p (sup @ l0) then |
|
104 |
min sup l0 |
|
105 |
else if p (sup @ r0) then |
|
106 |
min sup r0 |
|
107 |
else |
|
108 |
let |
|
109 |
val l = min (sup @ r0) l0 |
|
110 |
val r = min (sup @ l) r0 |
|
111 |
in l @ r end |
|
112 |
end |
|
113 |
val xs = |
|
114 |
case min [] xs of |
|
115 |
[x] => if p [] then [] else [x] |
|
116 |
| xs => xs |
|
117 |
in (xs, test xs) end |
|
118 |
||
119 |
(* Give the external prover some slack. The ATP gets further slack because the |
|
120 |
Sledgehammer preprocessing time is included in the estimate below but isn't |
|
121 |
part of the timeout. *) |
|
38590
bd443b426d56
get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
blanchet
parents:
38589
diff
changeset
|
122 |
val fudge_msecs = 1000 |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
123 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
124 |
fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." |
40065 | 125 |
| minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
126 |
state facts = |
31236 | 127 |
let |
36378 | 128 |
val thy = Proof.theory_of state |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40553
diff
changeset
|
129 |
val ctxt = Proof.context_of state |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40553
diff
changeset
|
130 |
val prover = get_prover ctxt false prover_name |
38590
bd443b426d56
get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
blanchet
parents:
38589
diff
changeset
|
131 |
val msecs = Time.toMilliseconds timeout |
40977 | 132 |
val _ = Output.urgent_message ("Sledgehammer minimize: " ^ |
133 |
quote prover_name ^ ".") |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
134 |
val {goal, ...} = Proof.goal state |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
135 |
val (_, hyp_ts, concl_t) = strip_subgoal goal i |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
136 |
val explicit_apply = |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
137 |
not (forall (Meson.is_fol_term thy) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
138 |
(concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
139 |
fun do_test timeout = |
40065 | 140 |
test_facts params prover explicit_apply timeout i n state |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
141 |
val timer = Timer.startRealTimer () |
31236 | 142 |
in |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
143 |
(case do_test timeout facts of |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
144 |
result as {outcome = NONE, used_facts, ...} => |
38015 | 145 |
let |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
146 |
val time = Timer.checkRealTimer timer |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
147 |
val new_timeout = |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
148 |
Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
149 |
|> Time.fromMilliseconds |
40977 | 150 |
val facts = filter_used_facts used_facts facts |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
151 |
val (min_thms, {message, ...}) = |
40977 | 152 |
if length facts >= binary_threshold then |
153 |
binary_minimize (do_test new_timeout) facts |
|
154 |
else |
|
155 |
sublinear_minimize (do_test new_timeout) facts ([], result) |
|
38094 | 156 |
val n = length min_thms |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
157 |
val _ = Output.urgent_message (cat_lines |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
158 |
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38745
diff
changeset
|
159 |
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
160 |
0 => "" |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
161 |
| n => " (including " ^ Int.toString n ^ " chained)") ^ ".") |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
162 |
in (SOME min_thms, message) end |
38015 | 163 |
| {outcome = SOME TimedOut, ...} => |
164 |
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \ |
|
165 |
\option (e.g., \"timeout = " ^ |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40205
diff
changeset
|
166 |
string_of_int (10 + msecs div 1000) ^ "\").") |
38015 | 167 |
| {outcome = SOME UnknownError, ...} => |
168 |
(* Failure sometimes mean timeout, unfortunately. *) |
|
169 |
(NONE, "Failure: No proof was found with the current time limit. You \ |
|
170 |
\can increase the time limit using the \"timeout\" \ |
|
171 |
\option (e.g., \"timeout = " ^ |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40205
diff
changeset
|
172 |
string_of_int (10 + msecs div 1000) ^ "\").") |
40977 | 173 |
| {message, ...} => (NONE, "Prover error: " ^ message)) |
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37926
diff
changeset
|
174 |
handle ERROR msg => (NONE, "Error: " ^ msg) |
31236 | 175 |
end |
176 |
||
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
177 |
fun run_minimize params i refs state = |
38045 | 178 |
let |
179 |
val ctxt = Proof.context_of state |
|
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38617
diff
changeset
|
180 |
val reserved = reserved_isar_keyword_table () |
38045 | 181 |
val chained_ths = #facts (Proof.goal state) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
182 |
val facts = |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
183 |
maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) refs |
38045 | 184 |
in |
185 |
case subgoal_count state of |
|
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
186 |
0 => Output.urgent_message "No subgoal!" |
38045 | 187 |
| n => |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39496
diff
changeset
|
188 |
(kill_provers (); |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
189 |
Output.urgent_message (#2 (minimize_facts params i n state facts))) |
38045 | 190 |
end |
191 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
192 |
end; |